:: Basic Properties of Determinants of Square Matrices over a Field
:: by Karol P\c{a}k
::
:: Received March 21, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

notation
let X be set ;
synonym  2Set X for  TWOELEMENTSETS X;
end;

theorem Th1: :: MATRIX11:1
for X being set
for n being Nat holds
( X in 2Set (Seg n) iff ex i, j being Nat st
( i in Seg n &amp; j in Seg n &amp; i < j &amp; X = {i,j} ) )
proofend;

theorem Th2: :: MATRIX11:2
( 2Set (Seg 0) = {} &amp; 2Set (Seg 1) = {} )
proofend;

theorem Th3: :: MATRIX11:3
for n being Nat st n >= 2 holds
{1,2} in 2Set (Seg n)
proofend;

registration
let n be Nat;
cluster 2Set (Seg (n + 2)) ->  non empty finite ;
coherence
 ( not 2Set (Seg (n + 2)) is empty &amp; 2Set (Seg (n + 2)) is finite )
proofend;
end;

registration
let n be Nat;
let x be set ;
let perm be Element of Permutations n;
clusterperm . x ->  natural ;
coherence
 perm . x is natural
proofend;
end;

registration
let K be Field;
cluster the multF of K ->  having_a_unity ;
coherence
 the multF of K is having_a_unity ;
cluster the multF of K ->  associative ;
coherence
 the multF of K is associative ;
end;

::------------------------------------------::
:: The partial sign of a permutation ::
::------------------------------------------::
definition
let n be Nat;
let K be Field;
let perm2 be Element of Permutations (n + 2);
func Part_sgn (perm2,K) ->  Function of (2Set (Seg (n + 2))), the carrier of K means :Def1: :: MATRIX11:def 1
 for i, j being Element of NAT st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j holds
( ( perm2 . i < perm2 . j implies it . {i,j} = 1_ K ) &amp; ( perm2 . i > perm2 . j implies it . {i,j} = - (1_ K) ) );
existence
 ex b1 being Function of (2Set (Seg (n + 2))), the carrier of K st
for i, j being Element of NAT st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j holds
( ( perm2 . i < perm2 . j implies b1 . {i,j} = 1_ K ) &amp; ( perm2 . i > perm2 . j implies b1 . {i,j} = - (1_ K) ) )
proofend;
uniqueness
 for b1, b2 being Function of (2Set (Seg (n + 2))), the carrier of K st ( for i, j being Element of NAT st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j holds
( ( perm2 . i < perm2 . j implies b1 . {i,j} = 1_ K ) &amp; ( perm2 . i > perm2 . j implies b1 . {i,j} = - (1_ K) ) ) ) &amp; ( for i, j being Element of NAT st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j holds
( ( perm2 . i < perm2 . j implies b2 . {i,j} = 1_ K ) &amp; ( perm2 . i > perm2 . j implies b2 . {i,j} = - (1_ K) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Part_sgn MATRIX11:def_1_:_
 for n being Nat
for K being Field
for perm2 being Element of Permutations (n + 2)
for b4 being Function of (2Set (Seg (n + 2))), the carrier of K holds
( b4 = Part_sgn (perm2,K) iff for i, j being Element of NAT st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j holds
( ( perm2 . i < perm2 . j implies b4 . {i,j} = 1_ K ) &amp; ( perm2 . i > perm2 . j implies b4 . {i,j} = - (1_ K) ) ) );

theorem Th4: :: MATRIX11:4
for n being Nat
for K being Field
for p2 being Element of Permutations (n + 2)
for X being Element of Fin (2Set (Seg (n + 2))) st ( for x being set st x in X holds
(Part_sgn (p2,K)) . x = 1_ K ) holds
the multF of K $$ (X,(Part_sgn (p2,K))) = 1_ K
proofend;

theorem Th5: :: MATRIX11:5
for n being Nat
for K being Field
for p2 being Element of Permutations (n + 2)
for s being Element of 2Set (Seg (n + 2)) holds
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )
proofend;

theorem Th6: :: MATRIX11:6
for n being Nat
for K being Field
for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j &amp; p2 . i = q2 . i &amp; p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
proofend;

theorem Th7: :: MATRIX11:7
for n being Nat
for K being Field
for X being Element of Fin (2Set (Seg (n + 2)))
for p2, q2 being Element of Permutations (n + 2)
for F being finite set st F =  {  s where s is Element of 2Set (Seg (n + 2)) : ( s in X &amp; (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s )  }  holds
( ( (card F) mod 2 = 0 implies the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K $$ (X,(Part_sgn (q2,K))) ) &amp; ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) )
proofend;

theorem Th8: :: MATRIX11:8
for n being Nat
for P being Permutation of (Seg n) st P is being_transposition holds
for i, j being Nat st i < j holds
( P . i = j iff ( i in dom P &amp; j in dom P &amp; P . i = j &amp; P . j = i &amp; ( for k being Nat st k <> i &amp; k <> j &amp; k in dom P holds
P . k = k ) ) )
proofend;

theorem Th9: :: MATRIX11:9
for n being Nat
for K being Field
for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 &amp; q2 is being_transposition &amp; q2 . i = j &amp; i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )
proofend;

Lm1:  for n being Nat
for K being Field
for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) &amp; j in Seg (n + 2) &amp; i < j &amp; 1_ K <> - (1_ K) holds
( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) &amp; ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )
proofend;

theorem Th10: :: MATRIX11:10
for n being Nat
for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat
for K being Field st pq2 = p2 * q2 &amp; q2 is being_transposition &amp; q2 . i = j &amp; i < j &amp; 1_ K <> - (1_ K) holds
( (Part_sgn (p2,K)) . {i,j} <> (Part_sgn (pq2,K)) . {i,j} &amp; ( for k being Nat st k in Seg (n + 2) &amp; i <> k &amp; j <> k holds
( (Part_sgn (p2,K)) . {i,k} <> (Part_sgn (pq2,K)) . {i,k} iff (Part_sgn (p2,K)) . {j,k} <> (Part_sgn (pq2,K)) . {j,k} ) ) )
proofend;

::------------------------------------------::
:: The sign of a permutation ::
::------------------------------------------::
definition
let n be Nat;
let K be Field;
let perm2 be Element of Permutations (n + 2);
func sgn (perm2,K) ->  Element of K equals :: MATRIX11:def 2
 the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));
coherence
 the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K))) is Element of K ;
end;

:: deftheorem  defines sgn MATRIX11:def_2_:_
 for n being Nat
for K being Field
for perm2 being Element of Permutations (n + 2) holds sgn (perm2,K) = the multF of K $$ ((FinOmega (2Set (Seg (n + 2)))),(Part_sgn (perm2,K)));

theorem Th11: :: MATRIX11:11
for n being Nat
for K being Field
for p2 being Element of Permutations (n + 2) holds
( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )
proofend;

theorem Th12: :: MATRIX11:12
for n being Nat
for K being Field
for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds
sgn (Id,K) = 1_ K
proofend;

Lm2:  for X being set
for n, i being Nat st X in 2Set (Seg n) &amp; i in X holds
( i in Seg n &amp; ex j being Nat st
( j in Seg n &amp; i <> j &amp; X = {i,j} ) )
proofend;

theorem Th13: :: MATRIX11:13
for n being Nat
for K being Field
for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 &amp; q2 is being_transposition holds
sgn (pq2,K) = - (sgn (p2,K))
proofend;

::------------------------------------------::
:: The sign of a transposition ::
::------------------------------------------::
theorem Th14: :: MATRIX11:14
for n being Nat
for K being Field
for tr being Element of Permutations (n + 2) st tr is being_transposition holds
sgn (tr,K) = - (1_ K)
proofend;

theorem Th15: :: MATRIX11:15
for n being Nat
for K being Field
for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P &amp; ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans &amp; trans is being_transposition ) ) holds
( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) &amp; ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
proofend;

theorem Th16: :: MATRIX11:16
for i, j, n being Nat st i < j &amp; i in Seg n &amp; j in Seg n holds
ex tr being Element of Permutations n st
( tr is being_transposition &amp; tr . i = j )
proofend;

theorem Th17: :: MATRIX11:17
for k being Nat
for p being Element of Permutations (k + 1) st p . (k + 1) <> k + 1 holds
ex tr being Element of Permutations (k + 1) st
( tr is being_transposition &amp; tr . (p . (k + 1)) = k + 1 &amp; (tr * p) . (k + 1) = k + 1 )
proofend;

theorem Th18: :: MATRIX11:18
for X, x being set st not x in X holds
for p1 being Permutation of (X \/ {x}) st p1 . x = x holds
ex p being Permutation of X st p1 | X = p
proofend;

theorem Th19: :: MATRIX11:19
for X, x being set
for p, q being Permutation of X
for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p &amp; q1 | X = q &amp; p1 . x = x &amp; q1 . x = x holds
( (p1 * q1) | X = p * q &amp; (p1 * q1) . x = x )
proofend;

theorem Th20: :: MATRIX11:20
for k being Nat
for tr being Element of Permutations k st tr is being_transposition holds
( tr * tr = idseq k &amp; tr = tr " )
proofend;

::------------------------------------------::
:: A general theorem about ::
:: the representation of a permutation as ::
:: a product of transpositions ::
::------------------------------------------::
theorem Th21: :: MATRIX11:21
for n being Nat
for perm being Element of Permutations n ex P being FinSequence of (Group_of_Perm n) st
( perm = Product P &amp; ( for i being Nat st i in dom P holds
ex trans being Element of Permutations n st
( P . i = trans &amp; trans is being_transposition ) ) )
proofend;

theorem Th22: :: MATRIX11:22
for K being Field holds
( K is Fanoian iff 1_ K <> - (1_ K) )
proofend;

::------------------------------------------::
:: The relation between sign and parity ::
:: of permutations ::
::------------------------------------------::
theorem Th23: :: MATRIX11:23
for n being Nat
for perm2 being Element of Permutations (n + 2)
for K being Fanoian Field holds
( ( perm2 is even implies sgn (perm2,K) = 1_ K ) &amp; ( sgn (perm2,K) = 1_ K implies perm2 is even ) &amp; ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) &amp; ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
proofend;

::------------------------------------------::
:: The sign of a composition of ::
:: permutations ::
::------------------------------------------::
theorem Th24: :: MATRIX11:24
for n being Nat
for K being Field
for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 holds
sgn (pq2,K) = (sgn (p2,K)) * (sgn (q2,K))
proofend;

Lm3:  for n being Nat
for p being Element of Permutations n st n < 2 holds
( p is even &amp; p = idseq n )
proofend;

theorem Th25: :: MATRIX11:25
for n being Nat
for p, q being Element of Permutations n holds
( ( ( p is even &amp; q is even ) or ( p is odd &amp; q is odd ) ) iff p * q is even )
proofend;

theorem Th26: :: MATRIX11:26
for n being Nat
for K being Field
for a being Element of K
for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a
proofend;

theorem Th27: :: MATRIX11:27
for n being Nat
for tr being Element of Permutations (n + 2) st tr is being_transposition holds
tr is odd
proofend;

registration
let n be Nat;
cluster Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite odd for Element of bool [:(Seg (n + 2)),(Seg (n + 2)):];
existence
 ex b1 being Permutation of (Seg (n + 2)) st b1 is odd
proofend;
end;

begin

definition
let l, n, m be Nat;
let D be non empty set ;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
func ReplaceLine (M,l,pD) ->  Matrix of n,m,D means :Def3: :: MATRIX11:def 3
( len it = len M &amp; width it = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies it * (i,j) = M * (i,j) ) &amp; ( i = l implies it * (l,j) = pD . j ) ) ) ) if  len pD = width M
otherwise it = M;
consistency
 for b1 being Matrix of n,m,D holds verum ;
existence
 ( ( len pD = width M implies ex b1 being Matrix of n,m,D st
( len b1 = len M &amp; width b1 = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * (i,j) = M * (i,j) ) &amp; ( i = l implies b1 * (l,j) = pD . j ) ) ) ) ) &amp; ( not len pD = width M implies ex b1 being Matrix of n,m,D st b1 = M ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,D holds
( ( len pD = width M &amp; len b1 = len M &amp; width b1 = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * (i,j) = M * (i,j) ) &amp; ( i = l implies b1 * (l,j) = pD . j ) ) ) &amp; len b2 = len M &amp; width b2 = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b2 * (i,j) = M * (i,j) ) &amp; ( i = l implies b2 * (l,j) = pD . j ) ) ) implies b1 = b2 ) &amp; ( not len pD = width M &amp; b1 = M &amp; b2 = M implies b1 = b2 ) )
proofend;
end;

:: deftheorem Def3 defines ReplaceLine MATRIX11:def_3_:_
 for l, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for pD being FinSequence of D
for b7 being Matrix of n,m,D holds
( ( len pD = width M implies ( b7 = ReplaceLine (M,l,pD) iff ( len b7 = len M &amp; width b7 = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b7 * (i,j) = M * (i,j) ) &amp; ( i = l implies b7 * (l,j) = pD . j ) ) ) ) ) ) &amp; ( not len pD = width M implies ( b7 = ReplaceLine (M,l,pD) iff b7 = M ) ) );

notation
let l, n, m be Nat;
let D be non empty set ;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
synonym  RLine (M,l,pD) for  ReplaceLine (M,l,pD);
end;

Lm4:  for m, n being Nat
for D being non empty set
for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D holds
( Indices M = Indices (RLine (M,l,pD)) &amp; len M = len (RLine (M,l,pD)) &amp; width M = width (RLine (M,l,pD)) )
proofend;

theorem Th28: :: MATRIX11:28
for m, n being Nat
for D being non empty set
for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg n holds
( ( i = l &amp; len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) &amp; ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
proofend;

theorem :: MATRIX11:29
for m, n, l being Nat
for D being non empty set
for M being Matrix of n,m,D
for pD being FinSequence of D st len pD = width M holds
for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9)
proofend;

theorem Th30: :: MATRIX11:30
for n, m, l being Nat
for D being non empty set
for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))
proofend;

Lm5:  for K being Field
for pK being FinSequence of K
for a being Element of K holds len pK = len (a * pK)
proofend;

Lm6:  for K being Field
for pK, qK being FinSequence of K st len pK = len qK holds
len pK = len (pK + qK)
proofend;

theorem Th31: :: MATRIX11:31
for n being Nat
for K being Field
for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n &amp; len pK = n &amp; len qK = n holds
for M being Matrix of n,K holds the multF of K $$ (Path_matrix (perm,(RLine (M,l,((a * pK) + (b * qK)))))) = (a * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,pK)))))) + (b * ( the multF of K $$ (Path_matrix (perm,(RLine (M,l,qK))))))
proofend;

theorem Th32: :: MATRIX11:32
for n being Nat
for K being Field
for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K
for perm being Element of Permutations n st l in Seg n &amp; len pK = n &amp; len qK = n holds
for M being Matrix of n,K holds (Path_product (RLine (M,l,((a * pK) + (b * qK))))) . perm = (a * ((Path_product (RLine (M,l,pK))) . perm)) + (b * ((Path_product (RLine (M,l,qK))) . perm))
proofend;

::------------------------------------------::
:: The determinant of a linear ::
:: combination of lines ::
::------------------------------------------::
theorem Th33: :: MATRIX11:33
for n being Nat
for K being Field
for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K st l in Seg n &amp; len pK = n &amp; len qK = n holds
for M being Matrix of n,K holds Det (RLine (M,l,((a * pK) + (b * qK)))) = (a * (Det (RLine (M,l,pK)))) + (b * (Det (RLine (M,l,qK))))
proofend;

theorem Th34: :: MATRIX11:34
for l, n being Nat
for K being Field
for a being Element of K
for pK being FinSequence of K
for A being Matrix of n,K st l in Seg n &amp; len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
proofend;

theorem :: MATRIX11:35
for l, n being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st l in Seg n holds
Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det A)
proofend;

theorem Th36: :: MATRIX11:36
for l, n being Nat
for K being Field
for pK, qK being FinSequence of K
for A being Matrix of n,K st l in Seg n &amp; len pK = n &amp; len qK = n holds
Det (RLine (A,l,(pK + qK))) = (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK)))
proofend;

Lm7:  for n, m being Nat
for D being non empty set
for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds M * F is Matrix of n,m,D
proofend;

begin

:: and with a Repeated Line
definition
let n, m be Nat;
let D be non empty set ;
let F be Function of (Seg n),(Seg n);
let M be Matrix of n,m,D;
:: original:*
redefine funcM * F ->  Matrix of n,m,D means :Def4: :: MATRIX11:def 4
( len it = len M &amp; width it = width M &amp; ( for i, j, k being Nat st [i,j] in Indices M &amp; F . i = k holds
it * (i,j) = M * (k,j) ) );
compatibility
 for b1 being Matrix of n,m,D holds
( b1 = F * M iff ( len b1 = len M &amp; width b1 = width M &amp; ( for i, j, k being Nat st [i,j] in Indices M &amp; F . i = k holds
b1 * (i,j) = M * (k,j) ) ) )
proofend;
correctness
coherence
F * M is Matrix of n,m,D;
by Lm7;
end;

:: deftheorem Def4 defines * MATRIX11:def_4_:_
 for n, m being Nat
for D being non empty set
for F being Function of (Seg n),(Seg n)
for M, b6 being Matrix of n,m,D holds
( b6 = M * F iff ( len b6 = len M &amp; width b6 = width M &amp; ( for i, j, k being Nat st [i,j] in Indices M &amp; F . i = k holds
b6 * (i,j) = M * (k,j) ) ) );

theorem Th37: :: MATRIX11:37
for n, m being Nat
for D being non empty set
for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds
( Indices M = Indices (M * F) &amp; ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k &amp; [k,j] in Indices M &amp; (M * F) * (i,j) = M * (k,j) ) ) )
proofend;

theorem Th38: :: MATRIX11:38
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for F being Function of (Seg n),(Seg n)
for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)
proofend;

theorem Th39: :: MATRIX11:39
for m, n being Nat
for D being non empty set
for M being Matrix of n,m,D holds M * (idseq n) = M
proofend;

theorem Th40: :: MATRIX11:40
for n being Nat
for K being Field
for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm
proofend;

theorem Th41: :: MATRIX11:41
for n being Nat
for K being Field
for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
the multF of K $$ (Path_matrix (p,(A * Perm))) = the multF of K $$ (Path_matrix (q,A))
proofend;

theorem Th42: :: MATRIX11:42
for n being Nat
for K being Field
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 " holds
sgn (p2,K) = sgn (q2,K)
proofend;

theorem Th43: :: MATRIX11:43
for n being Nat
for K being Field
for M being Matrix of n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
for p2, q2 being Element of Permutations (n + 2) st q2 = p2 * (Perm2 ") holds
(Path_product M) . q2 = (sgn (perm2,K)) * ((Path_product (M * Perm2)) . p2)
proofend;

theorem Th44: :: MATRIX11:44
for n being Nat
for perm being Element of Permutations n ex P being Permutation of (Permutations n) st
for p being Element of Permutations n holds P . p = p * perm
proofend;

theorem Th45: :: MATRIX11:45
for n being Nat
for K being Field
for M being Matrix of n + 2,n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
proofend;

::------------------------------------------::
:: The determinant of a matrix with ::
:: permutated lines ::
::------------------------------------------::
theorem Th46: :: MATRIX11:46
for n being Nat
for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
proofend;

theorem Th47: :: MATRIX11:47
for n being Nat
for PERM being Permutation of (Permutations n)
for perm being Element of Permutations n st perm is odd &amp; ( for p being Element of Permutations n holds PERM . p = p * perm ) holds
PERM .:  {  p where p is Element of Permutations n : p is even  }  =  {  q where q is Element of Permutations n : q is odd  }
proofend;

Lm8:  for n, i, j being Nat st i in Seg n &amp; j in Seg n &amp; i < j holds
ex ODD, EVEN being finite set st
( EVEN =  {  p where p is Element of Permutations n : p is even  }  &amp; ODD =  {  q where q is Element of Permutations n : q is odd  }  &amp; EVEN /\ ODD = {} &amp; EVEN \/ ODD = Permutations n &amp; ex PERM being Function of EVEN,ODD ex perm being Element of Permutations n st
( perm is being_transposition &amp; perm . i = j &amp; dom PERM = EVEN &amp; PERM is bijective &amp; ( for p being Element of Permutations n st p in EVEN holds
PERM . p = p * perm ) ) )
proofend;

theorem :: MATRIX11:48
for n being Nat st n >= 2 holds
ex ODD, EVEN being finite set st
( EVEN =  {  p where p is Element of Permutations n : p is even  }  &amp; ODD =  {  q where q is Element of Permutations n : q is odd  }  &amp; EVEN /\ ODD = {} &amp; EVEN \/ ODD = Permutations n &amp; card EVEN = card ODD )
proofend;

theorem Th49: :: MATRIX11:49
for n being Nat
for K being Field
for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
for p, q, tr being Element of Permutations n st q = p * tr &amp; tr is being_transposition &amp; tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
proofend;

::------------------------------------------::
:: The determinant of a matrix with ::
:: a repeated line ::
::------------------------------------------::
theorem Th50: :: MATRIX11:50
for n being Nat
for K being Field
for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
proofend;

theorem Th51: :: MATRIX11:51
for n being Nat
for K being Field
for A being Matrix of n,K
for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i <> j holds
Det (RLine (A,i,(Line (A,j)))) = 0. K
proofend;

theorem Th52: :: MATRIX11:52
for n being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
proofend;

theorem :: MATRIX11:53
for n being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i <> j holds
Det A = Det (RLine (A,i,((Line (A,i)) + (a * (Line (A,j))))))
proofend;

theorem Th54: :: MATRIX11:54
for n being Nat
for K being Field
for F being Function of (Seg n),(Seg n)
for A being Matrix of n,K st not F in Permutations n holds
Det (A * F) = 0. K
proofend;

begin

definition
let K be non empty addLoopStr ;
func addFinS K ->  BinOp of ( the carrier of K *) means :Def5: :: MATRIX11:def 5
 for p1, p2 being Element of the carrier of K * holds it . (p1,p2) = p1 + p2;
existence
 ex b1 being BinOp of ( the carrier of K *) st
for p1, p2 being Element of the carrier of K * holds b1 . (p1,p2) = p1 + p2
proofend;
uniqueness
 for b1, b2 being BinOp of ( the carrier of K *) st ( for p1, p2 being Element of the carrier of K * holds b1 . (p1,p2) = p1 + p2 ) &amp; ( for p1, p2 being Element of the carrier of K * holds b2 . (p1,p2) = p1 + p2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines addFinS MATRIX11:def_5_:_
 for K being non empty addLoopStr
for b2 being BinOp of ( the carrier of K *) holds
( b2 = addFinS K iff for p1, p2 being Element of the carrier of K * holds b2 . (p1,p2) = p1 + p2 );

Lm9:  for K being non empty addLoopStr
for p1, p2 being Element of the carrier of K * holds dom (p1 + p2) = (dom p1) /\ (dom p2)
proofend;

registration
let K be non empty Abelian addLoopStr ;
cluster addFinS K ->  commutative ;
coherence
 addFinS K is commutative
proofend;
end;

registration
let K be non empty add-associative addLoopStr ;
cluster addFinS K ->  associative ;
coherence
 addFinS K is associative
proofend;
end;

theorem Th55: :: MATRIX11:55
for K being Field
for A, B being Matrix of K st width A = len B &amp; len B > 0 holds
for i being Nat st i in Seg (len A) holds
ex P being FinSequence of the carrier of K * st
( len P = len B &amp; Line ((A * B),i) = (addFinS K) "**" P &amp; ( for j being Nat st j in Seg (len B) holds
P . j = (A * (i,j)) * (Line (B,j)) ) )
proofend;

theorem Th56: :: MATRIX11:56
for n being Nat
for K being Field
for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n &amp; Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P &amp; ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
proofend;

theorem Th57: :: MATRIX11:57
for X being set
for Y being non empty set
for x being set st not x in X holds
ex BIJECT being Function of [:(Funcs (X,Y)),Y:],(Funcs ((X \/ {x}),Y)) st
( BIJECT is bijective &amp; ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . (f,(F . x)) = F ) )
proofend;

theorem Th58: :: MATRIX11:58
for D being non empty set
for X being finite set
for Y being non empty finite set
for x being set st not x in X holds
for F being BinOp of D st F is having_a_unity &amp; F is commutative &amp; F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( for H being Function of X,Y
for SF being Element of Fin (Funcs ((X \/ {x}),Y)) st SF =  {  h where h is Function of (X \/ {x}),Y : h | X = H  }  holds
F $$ (SF,g) = f . H ) holds
F $$ ((FinOmega (Funcs (X,Y))),f) = F $$ ((FinOmega (Funcs ((X \/ {x}),Y))),g)
proofend;

theorem Th59: :: MATRIX11:59
for n, m being Nat
for D being non empty set
for A, B being Matrix of n,m,D
for i being Nat st i <= n &amp; 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) &amp; ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) &amp; ( not j in Seg i implies M . j = A . j ) ) ) )
proofend;

Lm10:  for n being Nat
for K being Field
for A, B being Matrix of n,n,K
for i being Nat st i <= n &amp; 0 < n holds
ex P being Function of (Funcs ((Seg i),(Seg n))), the carrier of K st
for F being Function of (Seg i),(Seg n)
for M being Matrix of n,n,K st M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg i)) &amp; ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) &amp; ( not j in Seg i implies M . j = (A * B) . j ) ) ) holds
ex Path being FinSequence of K st
( len Path = i &amp; ( for Fj, j being Nat st j in Seg i &amp; Fj = F . j holds
Path . j = A * (j,Fj) ) &amp; P . F = ( the multF of K $$ Path) * (Det M) )
proofend;

theorem Th60: :: MATRIX11:60
for n being Nat
for K being Field
for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Funcs ((Seg n),(Seg n))), the carrier of K st
( ( for F being Function of (Seg n),(Seg n) ex Path being FinSequence of K st
( len Path = n &amp; ( for Fj, j being Nat st j in Seg n &amp; Fj = F . j holds
Path . j = A * (j,Fj) ) &amp; P . F = ( the multF of K $$ Path) * (Det (B * F)) ) ) &amp; Det (A * B) = the addF of K $$ ((FinOmega (Funcs ((Seg n),(Seg n)))),P) )
proofend;

theorem Th61: :: MATRIX11:61
for n being Nat
for K being Field
for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((FinOmega (Permutations n)),P) &amp; ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
proofend;

::------------------------------------------::
:: Determinant of a product of ::
:: two square matrices ::
::------------------------------------------::
theorem :: MATRIX11:62
for n being Nat
for K being Field
for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)
proofend;