:: 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 & j in Seg n & i < j & X = {i,j} ) )
proof end;

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

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

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

registration
let n be Nat;
let x be set ;
let perm be Element of Permutations n;
cluster perm . x -> natural ;
coherence
perm . x is natural
proof end;
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) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies it . {i,j} = 1_ K ) & ( 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) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies b1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b1 . {i,j} = - (1_ K) ) )
proof end;
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) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies b1 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b1 . {i,j} = - (1_ K) ) ) ) & ( for i, j being Element of NAT st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies b2 . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b2 . {i,j} = - (1_ K) ) ) ) holds
b1 = b2
proof end;
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) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies b4 . {i,j} = 1_ K ) & ( 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
proof end;

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

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) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
proof end;

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 & (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))) ) & ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) )
proof end;

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 & j in dom P & P . i = j & P . j = i & ( for k being Nat st k <> i & k <> j & k in dom P holds
P . k = k ) ) )
proof end;

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 & q2 is being_transposition & q2 . i = j & 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 )
proof end;

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) & j in Seg (n + 2) & i < j & 1_ K <> - (1_ K) holds
( ( (Part_sgn (p2,K)) . {i,j} = 1_ K implies p2 . i < p2 . j ) & ( (Part_sgn (p2,K)) . {i,j} = - (1_ K) implies p2 . i > p2 . j ) )

proof end;

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 & q2 is being_transposition & q2 . i = j & i < j & 1_ K <> - (1_ K) holds
( (Part_sgn (p2,K)) . {i,j} <> (Part_sgn (pq2,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & 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} ) ) )
proof end;

::------------------------------------------::
:: 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) )
proof end;

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
proof end;

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

proof end;

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 & q2 is being_transposition holds
sgn (pq2,K) = - (sgn (p2,K))
proof end;

::------------------------------------------::
:: 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)
proof end;

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 & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) holds
( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
proof end;

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

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 & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )
proof end;

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
proof end;

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 & q1 | X = q & p1 . x = x & q1 . x = x holds
( (p1 * q1) | X = p * q & (p1 * q1) . x = x )
proof end;

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 & tr = tr " )
proof end;

::------------------------------------------::
:: 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 & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations n st
( P . i = trans & trans is being_transposition ) ) )
proof end;

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

::------------------------------------------::
:: 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 ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
proof end;

::------------------------------------------::
:: 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))
proof end;

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

proof end;

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

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
proof end;

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
proof end;

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
proof end;
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 & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies it * (i,j) = M * (i,j) ) & ( 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 & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * (i,j) = M * (i,j) ) & ( i = l implies b1 * (l,j) = pD . j ) ) ) ) ) & ( not len pD = width M implies ex b1 being Matrix of n,m,D st b1 = M ) )
proof end;
uniqueness
for b1, b2 being Matrix of n,m,D holds
( ( len pD = width M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b1 * (i,j) = M * (i,j) ) & ( i = l implies b1 * (l,j) = pD . j ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b2 * (i,j) = M * (i,j) ) & ( i = l implies b2 * (l,j) = pD . j ) ) ) implies b1 = b2 ) & ( not len pD = width M & b1 = M & b2 = M implies b1 = b2 ) )
proof end;
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 & width b7 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b7 * (i,j) = M * (i,j) ) & ( i = l implies b7 * (l,j) = pD . j ) ) ) ) ) ) & ( 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)) & len M = len (RLine (M,l,pD)) & width M = width (RLine (M,l,pD)) )

proof end;

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 & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
proof end;

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

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

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

proof end;

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

proof end;

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 & len pK = n & 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))))))
proof end;

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 & len pK = n & 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))
proof end;

::------------------------------------------::
:: 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 & len pK = n & 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))))
proof end;

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 & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
proof end;

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

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 & len pK = n & len qK = n holds
Det (RLine (A,l,(pK + qK))) = (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK)))
proof end;

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

proof end;

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 func M * F -> Matrix of n,m,D means :Def4: :: MATRIX11:def 4
( len it = len M & width it = width M & ( for i, j, k being Nat st [i,j] in Indices M & 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 & width b1 = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
b1 * (i,j) = M * (k,j) ) ) )
proof end;
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 & width b6 = width M & ( for i, j, k being Nat st [i,j] in Indices M & 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) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )
proof end;

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

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
proof end;

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
proof end;

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

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

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

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
proof end;

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

::------------------------------------------::
:: 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)
proof end;

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 & ( 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 }
proof end;

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

proof end;

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 } & ODD = { q where q is Element of Permutations n : q is odd } & EVEN /\ ODD = {} & EVEN \/ ODD = Permutations n & card EVEN = card ODD )
proof end;

theorem Th49: :: MATRIX11:49
for n being Nat
for K being Field
for i, j being Nat st i in Seg n & j in Seg n & 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 & tr is being_transposition & tr . i = j holds
(Path_product M) . q = - ((Path_product M) . p)
proof end;

::------------------------------------------::
:: 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 & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
proof end;

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 & j in Seg n & i <> j holds
Det (RLine (A,i,(Line (A,j)))) = 0. K
proof end;

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 & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
proof end;

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 & j in Seg n & i <> j holds
Det A = Det (RLine (A,i,((Line (A,i)) + (a * (Line (A,j))))))
proof end;

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
proof end;

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
proof end;
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 ) & ( for p1, p2 being Element of the carrier of K * holds b2 . (p1,p2) = p1 + p2 ) holds
b1 = b2
proof end;
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)

proof end;

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

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

theorem Th55: :: MATRIX11:55
for K being Field
for A, B being Matrix of K st width A = len B & 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 & Line ((A * B),i) = (addFinS K) "**" P & ( for j being Nat st j in Seg (len B) holds
P . j = (A * (i,j)) * (Line (B,j)) ) )
proof end;

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 & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
proof end;

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 & ( 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 ) )
proof end;

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 & F is commutative & 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)
proof end;

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 & 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)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
proof end;

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 & 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)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = (A * B) . j ) ) ) holds
ex Path being FinSequence of K st
( len Path = i & ( for Fj, j being Nat st j in Seg i & Fj = F . j holds
Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det M) )

proof end;

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 & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds
Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det (B * F)) ) ) & Det (A * B) = the addF of K $$ ((FinOmega (Funcs ((Seg n),(Seg n)))),P) )
proof end;

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) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
proof end;

::------------------------------------------::
:: 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)
proof end;