:: The Product of Matrices of Elements of a Field and Determinants
:: by Katarzyna Zawadzka
::
:: Received May 17, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

definition
let K be Field;
let n, m be Nat;
func 0. (K,n,m) ->  Matrix of n,m,K equals :: MATRIX_3:def 1
n |-> (m |-> (0. K));
coherence
 n |-> (m |-> (0. K)) is Matrix of n,m,K by MATRIX_1:10;
end;

:: deftheorem  defines 0. MATRIX_3:def_1_:_
 for K being Field
for n, m being Nat holds 0. (K,n,m) = n |-> (m |-> (0. K));

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)) ) )
proofend;
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
proofend;
end;

:: deftheorem Def2 defines - MATRIX_3:def_2_:_
 for K being Field
for A, b3 being Matrix of K holds
( b3 = - A iff ( len b3 = len A & width b3 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b3 * (i,j) = - (A * (i,j)) ) ) );

definition
let K be Field;
let A, B be Matrix of K;
funcA + 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)) ) )
proofend;
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
proofend;
end;

:: deftheorem Def3 defines + MATRIX_3:def_3_:_
 for K being Field
for A, B, b4 being Matrix of K holds
( b4 = A + B iff ( len b4 = len A & width b4 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b4 * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) );

theorem Th1: :: MATRIX_3:1
for n, m being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds
(0. (K,n,m)) * (i,j) = 0. K
proofend;

theorem :: MATRIX_3:2
for K being Field
for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
proofend;

theorem :: MATRIX_3:3
for K being Field
for A, B, C being Matrix of K st len A = len B & width A = width B holds
(A + B) + C = A + (B + C)
proofend;

theorem :: MATRIX_3:4
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (0. (K,n,m)) = A
proofend;

theorem :: MATRIX_3:5
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
proofend;

definition
let K be Field;
let A, B be Matrix of K;
assume A1: width A = len B ;
funcA * 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)) ) )
proofend;
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
proofend;
end;

:: deftheorem Def4 defines * MATRIX_3:def_4_:_
 for K being Field
for A, B being Matrix of K st width A = len B holds
for b4 being Matrix of K holds
( b4 = A * B iff ( len b4 = len A & width b4 = width B & ( for i, j being Nat st [i,j] in Indices b4 holds
b4 * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) );

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 funcA * B ->  Matrix of len A, width B,K;
coherence
 A * B is Matrix of len A, width B,K
proofend;
end;

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
funca * 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)) ) )
proofend;
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
proofend;
end;

:: deftheorem  defines * MATRIX_3:def_5_:_
 for K being Field
for M being Matrix of K
for a being Element of K
for b4 being Matrix of K holds
( b4 = a * M iff ( len b4 = len M & width b4 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = a * (M * (i,j)) ) ) );

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
funcM * a ->  Matrix of K equals :: MATRIX_3:def 6
a * M;
coherence
 a * M is Matrix of K ;
end;

:: deftheorem  defines * MATRIX_3:def_6_:_
 for K being Field
for M being Matrix of K
for a being Element of K holds M * a = a * M;

theorem :: MATRIX_3:6
for K being Field
for p, q being FinSequence of K st len p = len q holds
( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )
proofend;

theorem :: MATRIX_3:7
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds
(Line ((1. (K,n)),i)) . l = 1. K
proofend;

theorem :: MATRIX_3:8
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. (K,n)) &amp; l <> i holds
(Line ((1. (K,n)),i)) . l = 0. K
proofend;

theorem :: MATRIX_3:9
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) &amp; l = j holds
(Col ((1. (K,n)),j)) . l = 1. K
proofend;

theorem :: MATRIX_3:10
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. (K,n)) &amp; l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
proofend;

Lm1:  for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proofend;

theorem Th11: :: MATRIX_3:11
for n being Element of NAT
for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K
proofend;

theorem Th12: :: MATRIX_3:12
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of K
for i being Nat st i in dom p &amp; ( for k being Nat st k in dom p &amp; k <> i holds
p . k = 0. K ) holds
Sum p = p . i
proofend;

theorem Th13: :: MATRIX_3:13
for K being Field
for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))
proofend;

theorem Th14: :: MATRIX_3:14
for K being Field
for p, q being FinSequence of K
for i being Nat st p . i = 1. K &amp; ( for k being Nat st k in dom p &amp; k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt (p,q)) holds
( ( i = j implies (mlt (p,q)) . j = q . i ) &amp; ( i <> j implies (mlt (p,q)) . j = 0. K ) )
proofend;

theorem Th15: :: MATRIX_3:15
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) &amp; ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
proofend;

theorem Th16: :: MATRIX_3:16
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) &amp; ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )
proofend;

theorem Th17: :: MATRIX_3:17
for K being Field
for p, q being FinSequence of K
for i being Nat st i in dom p &amp; i in dom q &amp; p . i = 1. K &amp; ( for k being Nat st k in dom p &amp; k <> i holds
p . k = 0. K ) holds
Sum (mlt (p,q)) = q . i
proofend;

theorem :: MATRIX_3:18
for n being Nat
for K being Field
for A being Matrix of n,K holds (1. (K,n)) * A = A
proofend;

theorem :: MATRIX_3:19
for n being Nat
for K being Field
for A being Matrix of n,K holds A * (1. (K,n)) = A
proofend;

theorem :: MATRIX_3:20
for K being Field
for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
proofend;

theorem :: MATRIX_3:21
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)))
proofend;

theorem :: MATRIX_3:22
for K being Field
for A, B being Matrix of K st width A = len B &amp; width B <> 0 holds
(A * B) @ = (B @) * (A @)
proofend;

begin

definition
let I, J be non empty set ;
let X be Element of Fin I;
let Y be Element of Fin J;
:: original:[:
redefine func[:X,Y:] ->  Element of Fin [:I,J:];
coherence
 [:X,Y:] is Element of Fin [:I,J:]
proofend;
end;

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 funcG * (f,g) ->  Function of [:I,J:],D;
coherence
 G * (f,g) is Function of [:I,J:],D by FINSEQOP:79;
end;

theorem Th23: :: MATRIX_3:23
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 &amp; F is associative &amp; ( [:Y,X:] <> {} or F is having_a_unity ) &amp; G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
proofend;

theorem Th24: :: MATRIX_3:24
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 &amp; F is associative 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)))))
proofend;

theorem Th25: :: MATRIX_3:25
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 &amp; F is associative &amp; F is having_a_unity &amp; F is having_an_inverseOp &amp; 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)))))
proofend;

theorem Th26: :: MATRIX_3:26
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 having_a_unity &amp; F is commutative &amp; F is associative &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))
proofend;

theorem :: MATRIX_3:27
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 &amp; F is associative &amp; 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)))
proofend;

theorem :: MATRIX_3:28
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 having_a_unity &amp; F is commutative &amp; F is associative &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F &amp; G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))
proofend;

theorem Th29: :: MATRIX_3:29
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity &amp; F is commutative &amp; F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
proofend;

theorem Th30: :: MATRIX_3:30
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) &amp; F is having_a_unity &amp; F is commutative &amp; F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)
proofend;

theorem Th31: :: MATRIX_3:31
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity &amp; F is commutative &amp; F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
proofend;

theorem Th32: :: MATRIX_3:32
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) &amp; F is having_a_unity &amp; F is commutative &amp; F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)
proofend;

theorem :: MATRIX_3:33
for K being Field
for A, B, C being Matrix of K st width A = len B &amp; width B = len C holds
(A * B) * C = A * (B * C)
proofend;

begin

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 &amp; ( for i, j being Nat st i in dom it &amp; j = p . i holds
it . i = M * (i,j) ) );
existence
 ex b1 being FinSequence of K st
( len b1 = n &amp; ( for i, j being Nat st i in dom b1 &amp; j = p . i holds
b1 . i = M * (i,j) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of K st len b1 = n &amp; ( for i, j being Nat st i in dom b1 &amp; j = p . i holds
b1 . i = M * (i,j) ) &amp; len b2 = n &amp; ( for i, j being Nat st i in dom b2 &amp; j = p . i holds
b2 . i = M * (i,j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Path_matrix MATRIX_3:def_7_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for p being Element of Permutations n
for b5 being FinSequence of K holds
( b5 = Path_matrix (p,M) iff ( len b5 = n &amp; ( for i, j being Nat st i in dom b5 &amp; j = p . i holds
b5 . i = M * (i,j) ) ) );

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 multF 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 multF of K $$ (Path_matrix (p,M))),p)
proofend;
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 multF of K $$ (Path_matrix (p,M))),p) ) &amp; ( for p being Element of Permutations n holds b2 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines Path_product MATRIX_3:def_8_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being Function of (Permutations n), the carrier of K holds
( b4 = Path_product M iff for p being Element of Permutations n holds b4 . p = - (( the multF of K $$ (Path_matrix (p,M))),p) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Det M ->  Element of K equals :: MATRIX_3:def 9
 the addF of K $$ ((FinOmega (Permutations n)),(Path_product M));
coherence
 the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) is Element of K ;
end;

:: deftheorem  defines Det MATRIX_3:def_9_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds Det M = the addF of K $$ ((FinOmega (Permutations n)),(Path_product M));

theorem :: MATRIX_3:34
for K being Field
for a being Element of K holds Det <*<*a*>*> = a
proofend;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func diagonal_of_Matrix M ->  FinSequence of K means :: MATRIX_3:def 10
( len it = n &amp; ( for i being Nat st i in Seg n holds
it . i = M * (i,i) ) );
existence
 ex b1 being FinSequence of K st
( len b1 = n &amp; ( for i being Nat st i in Seg n holds
b1 . i = M * (i,i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of K st len b1 = n &amp; ( for i being Nat st i in Seg n holds
b1 . i = M * (i,i) ) &amp; len b2 = n &amp; ( for i being Nat st i in Seg n holds
b2 . i = M * (i,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines diagonal_of_Matrix MATRIX_3:def_10_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being FinSequence of K holds
( b4 = diagonal_of_Matrix M iff ( len b4 = n &amp; ( for i being Nat st i in Seg n holds
b4 . i = M * (i,i) ) ) );