:: Basic Properties of Determinants of Square Matrices over a Field
:: by Karol P\c{a}k
::
:: Received March 21, 2007
:: Copyright (c) 2007-2021 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 (Seg 0) = {} & 2Set (Seg 1) = {} ) by FINSEQ_1:2;

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 b₁ 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 b₁ . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b₁ . {i,j} = - (1_ K) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b₁ . {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 b₂ . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b₂ . {i,j} = - (1_ K) ) ) ) holds
b₁ = b₂

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 b₄ being Function of (2Set (Seg (n + 2))), the carrier of K holds
( b₄ = 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 b₄ . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b₄ . {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 (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;

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

cluster non empty non degenerated right_complementable V120() unital associative commutative right-distributive left-distributive right_unital well-unital V169() left_unital Fanoian Abelian add-associative right_zeroed domRing-like for doubleLoopStr ;

existence
ex b₁ being Ring st
( b₁ is Fanoian & not b₁ is degenerated & b₁ is well-unital & b₁ is domRing-like & b₁ 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;

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 b₁ being Permutation of (Seg (n + 2)) st b₁ 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 b₁ being Matrix of n,m,D holds verum ;
existence
( ( len pD = width M implies ex b₁ being Matrix of n,m,D st
( len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b₁ * (i,j) = M * (i,j) ) & ( i = l implies b₁ * (l,j) = pD . j ) ) ) ) ) & ( not len pD = width M implies ex b₁ being Matrix of n,m,D st b₁ = M ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,D holds
( ( len pD = width M & len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b₁ * (i,j) = M * (i,j) ) & ( i = l implies b₁ * (l,j) = pD . j ) ) ) & len b₂ = len M & width b₂ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b₂ * (i,j) = M * (i,j) ) & ( i = l implies b₂ * (l,j) = pD . j ) ) ) implies b₁ = b₂ ) & ( not len pD = width M & b₁ = M & b₂ = M implies b₁ = b₂ ) )

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 b₇ being Matrix of n,m,D holds
( ( len pD = width M implies ( b₇ = ReplaceLine (M,l,pD) iff ( len b₇ = len M & width b₇ = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies b₇ * (i,j) = M * (i,j) ) & ( i = l implies b₇ * (l,j) = pD . j ) ) ) ) ) ) & ( not len pD = width M implies ( b₇ = ReplaceLine (M,l,pD) iff b₇ = 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 b₁ being Matrix of n,m,D holds
( b₁ = F * M iff ( len b₁ = len M & width b₁ = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
b₁ * (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, b₆ being Matrix of n,m,D holds
( b₆ = M * F iff ( len b₆ = len M & width b₆ = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
b₆ * (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 * (idseq n) = 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
(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 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 (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 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
(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 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 b₁ being BinOp of ( the carrier of K *) st
for p1, p2 being Element of the carrier of K * holds b₁ . (p1,p2) = p1 + p2

proof end;

uniqueness
for b₁, b₂ being BinOp of ( the carrier of K *) st ( for p1, p2 being Element of the carrier of K * holds b₁ . (p1,p2) = p1 + p2 ) & ( for p1, p2 being Element of the carrier of K * holds b₂ . (p1,p2) = p1 + p2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines addFinS MATRIX11:def 5 :
for K being non empty addLoopStr
for b₂ being BinOp of ( the carrier of K *) holds
( b₂ = addFinS K iff for p1, p2 being Element of the carrier of K * holds b₂ . (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 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) = (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 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 * ((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 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 * ((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 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 (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (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 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;