:: MATRIX_3 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for n, k being Nat st n = n + k holds
k = 0
by XCMPLX_1:3;
:: deftheorem defines 0. MATRIX_3:def 1 :
definition
let K be
Field;
let A be
Matrix of
K;
func - A -> Matrix of
K means :
Def2:
:: MATRIX_3:def 2
(
len it = len A &
width it = width A & ( for
i,
j being
Nat st
[i,j] in Indices A holds
it * i,
j = - (A * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j) ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = - (A * i,j) ) holds
b1 = b2
end;
:: deftheorem Def2 defines - MATRIX_3:def 2 :
definition
let K be
Field;
let A,
B be
Matrix of
K;
func A + B -> Matrix of
K means :
Def3:
:: MATRIX_3:def 3
(
len it = len A &
width it = width A & ( for
i,
j being
Nat st
[i,j] in Indices A holds
it * i,
j = (A * i,j) + (B * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j) ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = (A * i,j) + (B * i,j) ) holds
b1 = b2
end;
:: deftheorem Def3 defines + MATRIX_3:def 3 :
theorem :: MATRIX_3:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: MATRIX_3:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th3: :: MATRIX_3:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let K be
Field;
let A,
B be
Matrix of
K;
assume A1:
width A = len B
;
func A * B -> Matrix of
K means :
Def4:
:: MATRIX_3:def 4
(
len it = len A &
width it = width B & ( for
i,
j being
Nat st
[i,j] in Indices it holds
it * i,
j = (Line A,i) "*" (Col B,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = (Line A,i) "*" (Col B,j) ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = (Line A,i) "*" (Col B,j) ) & len b2 = len A & width b2 = width B & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * i,j = (Line A,i) "*" (Col B,j) ) holds
b1 = b2
end;
:: deftheorem Def4 defines * MATRIX_3:def 4 :
definition
let n,
k,
m be
Nat;
let K be
Field;
let A be
Matrix of
n,
k,
K;
let B be
Matrix of
width A,
m,
K;
:: original: *redefine func A * B -> Matrix of
len A,
width B,
K;
coherence
A * B is Matrix of len A, width B,K
end;
definition
let K be
Field;
let M be
Matrix of
K;
let a be
Element of
K;
func a * M -> Matrix of
K means :: MATRIX_3:def 5
(
len it = len M &
width it = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
it * i,
j = a * (M * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = a * (M * i,j) ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = a * (M * i,j) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = a * (M * i,j) ) holds
b1 = b2
end;
:: deftheorem defines * MATRIX_3:def 5 :
:: deftheorem defines * MATRIX_3:def 6 :
theorem :: MATRIX_3:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm2:
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of L st ( for i being Nat st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
theorem Th13: :: MATRIX_3:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: MATRIX_3:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: MATRIX_3:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: MATRIX_3:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: MATRIX_3:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: MATRIX_3:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: MATRIX_3:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
K being
Field for
a1,
a2,
b1,
b2,
c1,
c2,
d1,
d2 being
Element of
K holds
(a1,b1 ][ c1,d1) * (a2,b2 ][ c2,d2) = ((a1 * a2) + (b1 * c2)),
((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),
((c1 * b2) + (d1 * d2))
theorem :: MATRIX_3:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let I,
J,
D be non
empty set ;
let G be
BinOp of
D;
let f be
Function of
I,
D;
let g be
Function of
J,
D;
:: original: *redefine func G * f,
g -> Function of
[:I,J:],
D;
coherence
G * f,g is Function of [:I,J:],D
by FINSEQOP:84;
end;
theorem Th25: :: MATRIX_3:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
I,
J,
D being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D for
X being
Element of
Fin I for
Y being
Element of
Fin J st
F is
commutative &
F is
associative & (
[:Y,X:] <> {} or
F has_a_unity ) &
G is
commutative holds
F $$ [:X,Y:],
(G * f,g) = F $$ [:Y,X:],
(G * g,f)
theorem Th26: :: MATRIX_3:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
D,
I,
J being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D st
F is
commutative &
F is
associative &
F has_a_unity holds
for
x being
Element of
I for
y being
Element of
J holds
F $$ [:{x},{y}:],
(G * f,g) = F $$ {x},
(G [:] f,(F $$ {y},g))
theorem Th27: :: MATRIX_3:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
D,
I,
J being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D for
X being
Element of
Fin I for
Y being
Element of
Fin J st
F is
commutative &
F is
associative &
F has_a_unity &
F has_an_inverseOp &
G is_distributive_wrt F holds
for
x being
Element of
I holds
F $$ [:{x},Y:],
(G * f,g) = F $$ {x},
(G [:] f,(F $$ Y,g))
theorem Th28: :: MATRIX_3:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
D,
I,
J being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D for
X being
Element of
Fin I for
Y being
Element of
Fin J st
F has_a_unity &
F is
commutative &
F is
associative &
F has_an_inverseOp &
G is_distributive_wrt F holds
F $$ [:X,Y:],
(G * f,g) = F $$ X,
(G [:] f,(F $$ Y,g))
theorem :: MATRIX_3:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
D,
I,
J being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D st
F is
commutative &
F is
associative &
F has_a_unity &
G is
commutative holds
for
x being
Element of
I for
y being
Element of
J holds
F $$ [:{x},{y}:],
(G * f,g) = F $$ {y},
(G [;] (F $$ {x},f),g)
theorem :: MATRIX_3:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
D,
I,
J being non
empty set for
F,
G being
BinOp of
D for
f being
Function of
I,
D for
g being
Function of
J,
D for
X being
Element of
Fin I for
Y being
Element of
Fin J st
F has_a_unity &
F is
commutative &
F is
associative &
F has_an_inverseOp &
G is_distributive_wrt F &
G is
commutative holds
F $$ [:X,Y:],
(G * f,g) = F $$ Y,
(G [;] (F $$ X,f),g)
theorem Th31: :: MATRIX_3:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: MATRIX_3:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th33: :: MATRIX_3:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: MATRIX_3:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: MATRIX_3:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
let p be
Element of
Permutations n;
func Path_matrix p,
M -> FinSequence of
K means :
Def7:
:: MATRIX_3:def 7
(
len it = n & ( for
i,
j being
Nat st
i in dom it &
j = p . i holds
it . i = M * i,
j ) );
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * i,j ) )
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * i,j ) & len b2 = n & ( for i, j being Nat st i in dom b2 & j = p . i holds
b2 . i = M * i,j ) holds
b1 = b2
end;
:: deftheorem Def7 defines Path_matrix MATRIX_3:def 7 :
definition
let n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
func Path_product M -> Function of
Permutations n,the
carrier of
K means :
Def8:
:: MATRIX_3:def 8
for
p being
Element of
Permutations n holds
it . p = - (the mult of K $$ (Path_matrix p,M)),
p;
existence
ex b1 being Function of Permutations n,the carrier of K st
for p being Element of Permutations n holds b1 . p = - (the mult of K $$ (Path_matrix p,M)),p
uniqueness
for b1, b2 being Function of Permutations n,the carrier of K st ( for p being Element of Permutations n holds b1 . p = - (the mult of K $$ (Path_matrix p,M)),p ) & ( for p being Element of Permutations n holds b2 . p = - (the mult of K $$ (Path_matrix p,M)),p ) holds
b1 = b2
end;
:: deftheorem Def8 defines Path_product MATRIX_3:def 8 :
:: deftheorem defines Det MATRIX_3:def 9 :
theorem :: MATRIX_3:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines diagonal_of_Matrix MATRIX_3:def 10 :