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

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 () = {} & 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 object ;
let perm be Element of Permutations n;
cluster perm . x -> natural ;
coherence
perm . x is natural
proof end;
end;

registration
let K be commutative Ring;
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 commutative Ring;
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 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 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 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 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 commutative Ring
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 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 commutative Ring
for p2 being Element of Permutations (n + 2)
for X being Element of Fin (2Set (Seg (n + 2))) st ( for x being object 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 commutative Ring 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 commutative Ring 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 commutative Ring 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 commutative Ring 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 commutative Ring 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 commutative Ring 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 commutative Ring; let perm2 be Element of Permutations (n + 2); func sgn (perm2,K) -> Element of K equals :: MATRIX11:def 2 the multF of K$$ ((In ((2Set (Seg (n + 2))),(Fin (2Set (Seg (n + 2)))))),(Part_sgn (perm2,K)));
coherence
the multF of K $$((In ((2Set (Seg (n + 2))),(Fin (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 commutative Ring for perm2 being Element of Permutations (n + 2) holds sgn (perm2,K) = the multF of K$$ ((In ((2Set (Seg (n + 2))),(Fin (2Set (Seg (n + 2)))))),(Part_sgn (perm2,K)));

theorem Th11: :: MATRIX11:11
for n being Nat
for K being commutative Ring
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 commutative Ring
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 i, n 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 commutative Ring
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 commutative Ring
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 commutative Ring
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 being set
for x being object 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 being object
for 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 () 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;

th22: for K being commutative Ring st not K is degenerated & K is well-unital & K is Fanoian holds
1_ K <> - (1_ K)

proof end;

theorem Th22: :: MATRIX11:22
for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like 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 K being commutative Ring
for perm2 being Element of Permutations (n + 2) st K is Fanoian & not K is degenerated 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 commutative Ring
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;

registration
existence
ex b1 being Ring st
( b1 is Fanoian & not b1 is degenerated & b1 is well-unital & b1 is domRing-like & b1 is commutative )
proof end;
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 commutative Ring
for a being Element of K
for perm2 being Element of Permutations (n + 2) st not K is degenerated & K is well-unital & K is domRing-like 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;
existence
ex b1 being Permutation of (Seg (n + 2)) st b1 is odd
proof end;
end;

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 n, m 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 n, m 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 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 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 l, n, m 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 Ring
for pK being FinSequence of K
for a being Element of K holds len pK = len (a * pK)

proof end;

Lm6: for K being commutative Ring
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 commutative Ring
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 commutative Ring 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 commutative Ring 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 commutative Ring for pK being FinSequence of K for a being Element 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 commutative Ring 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 commutative Ring 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; :: 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 n, m being Nat for D being non empty set for M being Matrix of n,m,D holds M * () = M proof end; theorem Th40: :: MATRIX11:40 for n being Nat for K being commutative Ring 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 commutative Ring 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 commutative Ring st not K is degenerated & K is domRing-like holds 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 commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds 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 () . 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 () 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 commutative Ring st not K is degenerated & K is domRing-like & K is well-unital holds 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 commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds 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 () 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 commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds 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 () . q = - (() . p) proof end; ::------------------------------------------:: :: The determinant of a matrix with :: :: a repeated line :: ::------------------------------------------:: theorem Th50: :: MATRIX11:50 for n being Nat for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds 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 commutative Ring for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds 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 commutative Ring for a being Element of K for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds 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 commutative Ring for a being Element of K for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds 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 commutative Ring for F being Function of (Seg n),(Seg n) for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like & not F in Permutations n holds Det (A * F) = 0. K proof end; 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 ; coherence proof end; end; registration let K be non empty add-associative addLoopStr ; coherence proof end; end; theorem Th55: :: MATRIX11:55 for K being Ring 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) = () "**" 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 commutative Ring 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 object 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 object 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 $$((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F$$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (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 * (() +* 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 Ring
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 * (() +* 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 commutative Ring 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 $$((In ((Funcs ((Seg n),(Seg n))),(Fin (Funcs ((Seg n),(Seg n)))))),P) ) proof end; theorem Th61: :: MATRIX11:61 for n being Nat for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds for A, B being Matrix of n,K st 0 < n holds ex P being Function of (), the carrier of K st ( Det (A * B) = the addF of K$$ ((In ((),(Fin ()))),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 commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)
proof end;