:: On the Permanent of a Matrix
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received January 4, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: MATRIX_9:1
for a, A being set st a in A holds
{a} in Fin A
proofend;

registration
let n be Nat;
cluster non empty finite for Element of Fin (Permutations n);
existence
 not for b1 being Element of Fin (Permutations n) holds b1 is empty
proofend;
end;

scheme :: MATRIX_9:sch 1
NonEmptyFiniteX{ F1() ->  Element of NAT , F2() ->  non empty Element of Fin (Permutations F1()), P1[ set ] } :
 P1[F2()]
provided
A1: for x being Element of Permutations F1() st x in F2() holds
P1[{x}] and
A2: for x being Element of Permutations F1()
for B being non empty Element of Fin (Permutations F1()) st x in F2() & B c= F2() & not x in B & P1[B] holds
P1[B \/ {x}]
proofend;

Lm1:  <*1,2*> <> <*2,1*>
by FINSEQ_1:77;

Lm2:  <*2,1*> in Permutations 2
by MATRIX_7:3, TARSKI:def_2;

registration
let n be Nat;
cluster Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total finite FinSequence-like for Element of bool [:(Seg n),(Seg n):];
existence
 ex b1 being Function of (Seg n),(Seg n) st
( b1 is one-to-one &amp; b1 is FinSequence-like )
proofend;
end;

registration
let n be Nat;
cluster id (Seg n) ->  FinSequence-like ;
coherence
 id (Seg n) is FinSequence-like
proofend;
end;

theorem Th2: :: MATRIX_9:2
( (Rev (idseq 2)) . 1 = 2 &amp; (Rev (idseq 2)) . 2 = 1 )
proofend;

theorem Th3: :: MATRIX_9:3
for f being one-to-one Function st dom f = Seg 2 &amp; rng f = Seg 2 &amp; not f = id (Seg 2) holds
f = Rev (id (Seg 2))
proofend;

begin

theorem Th4: :: MATRIX_9:4
for n being Nat holds Rev (idseq n) in Permutations n
proofend;

theorem Th5: :: MATRIX_9:5
for n being Nat
for f being FinSequence st n <> 0 &amp; f in Permutations n holds
Rev f in Permutations n
proofend;

theorem Th6: :: MATRIX_9:6
Permutations 2 = {(idseq 2),(Rev (idseq 2))}
proofend;

begin

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func PPath_product M ->  Function of (Permutations n), the carrier of K means :Def1: :: MATRIX_9:def 1
 for p being Element of Permutations n holds it . p = the multF of K $$ (Path_matrix (p,M));
existence
 ex b1 being Function of (Permutations n), the carrier of K st
for p being Element of Permutations n holds b1 . p = the multF of K $$ (Path_matrix (p,M))
proofend;
uniqueness
 for b1, b2 being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b1 . p = the multF of K $$ (Path_matrix (p,M)) ) &amp; ( for p being Element of Permutations n holds b2 . p = the multF of K $$ (Path_matrix (p,M)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines PPath_product MATRIX_9:def_1_:_
 for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being Function of (Permutations n), the carrier of K holds
( b4 = PPath_product M iff for p being Element of Permutations n holds b4 . p = the multF of K $$ (Path_matrix (p,M)) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Per M ->  Element of K equals :: MATRIX_9:def 2
 the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M));
coherence
 the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) is Element of K ;
end;

:: deftheorem  defines Per MATRIX_9:def_2_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds Per M = the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M));

theorem :: MATRIX_9:7
for K being Field
for a being Element of K holds Per <*<*a*>*> = a
proofend;

theorem :: MATRIX_9:8
for K being Field
for n being Element of NAT st n >= 1 holds
Per (0. (K,n,n)) = 0. K
proofend;

theorem Th9: :: MATRIX_9:9
for K being Field
for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
proofend;

theorem Th10: :: MATRIX_9:10
for K being Field
for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = Rev (idseq 2) holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
proofend;

theorem Th11: :: MATRIX_9:11
for K being Field
for a, b being Element of K holds the multF of K $$ <*a,b*> = a * b
proofend;

begin

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

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

theorem Th12: :: MATRIX_9:12
<*2,1*> is odd Permutation of (Seg 2)
proofend;

theorem :: MATRIX_9:13
for K being Field
for a, b, c, d being Element of K holds Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
proofend;

theorem :: MATRIX_9:14
for K being Field
for a, b, c, d being Element of K holds Per ((a,b) ][ (c,d)) = (a * d) + (b * c)
proofend;

theorem Th15: :: MATRIX_9:15
Rev (idseq 3) = <*3,2,1*>
proofend;

theorem :: MATRIX_9:16
for D being non empty set
for x, y, z being Element of D
for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
proofend;

theorem Th17: :: MATRIX_9:17
for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
f ^ (Rev g) in Permutations n
proofend;

theorem Th18: :: MATRIX_9:18
for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
g ^ f in Permutations n
proofend;

theorem Th19: :: MATRIX_9:19
Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
proofend;

theorem Th20: :: MATRIX_9:20
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
proofend;

theorem Th21: :: MATRIX_9:21
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*>
proofend;

theorem Th22: :: MATRIX_9:22
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*>
proofend;

theorem Th23: :: MATRIX_9:23
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>
proofend;

theorem Th24: :: MATRIX_9:24
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*>
proofend;

theorem Th25: :: MATRIX_9:25
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>
proofend;

theorem Th26: :: MATRIX_9:26
for K being Field
for a, b, c being Element of K holds the multF of K $$ <*a,b,c*> = (a * b) * c
proofend;

theorem Th27: :: MATRIX_9:27
( <*1,3,2*> in Permutations 3 &amp; <*2,3,1*> in Permutations 3 &amp; <*2,1,3*> in Permutations 3 &amp; <*3,1,2*> in Permutations 3 &amp; <*1,2,3*> in Permutations 3 &amp; <*3,2,1*> in Permutations 3 )
proofend;

Lm3:  <*1,2,3*> <> <*3,2,1*>
by FINSEQ_1:78;

Lm4:  <*1,2,3*> <> <*1,3,2*>
by FINSEQ_1:78;

Lm5:  <*1,2,3*> <> <*2,1,3*>
by FINSEQ_1:78;

Lm6:  ( <*1,2,3*> <> <*2,3,1*> &amp; <*1,2,3*> <> <*3,1,2*> )
by FINSEQ_1:78;

Lm7:  ( <*3,2,1*> <> <*2,3,1*> &amp; <*3,2,1*> <> <*3,1,2*> )
by FINSEQ_1:78;

Lm8:  ( <*3,2,1*> <> <*2,1,3*> &amp; <*1,3,2*> <> <*2,1,3*> )
by FINSEQ_1:78;

Lm9:  ( <*1,3,2*> <> <*2,3,1*> &amp; <*1,3,2*> <> <*3,1,2*> )
by FINSEQ_1:78;

Lm10:  ( <*3,2,1*> <> <*1,3,2*> &amp; <*2,3,1*> <> <*3,1,2*> )
by FINSEQ_1:78;

Lm11:  ( <*2,3,1*> <> <*2,1,3*> &amp; <*2,1,3*> <> <*3,1,2*> )
by FINSEQ_1:78;

theorem Th28: :: MATRIX_9:28
<*2,3,1*> " = <*3,1,2*>
proofend;

theorem :: MATRIX_9:29
for a being Element of (Group_of_Perm 3) st a = <*2,3,1*> holds
a " = <*3,1,2*>
proofend;

begin

theorem Th30: :: MATRIX_9:30
for p being Permutation of (Seg 3) st p = <*1,3,2*> holds
p is being_transposition
proofend;

theorem Th31: :: MATRIX_9:31
for p being Permutation of (Seg 3) st p = <*2,1,3*> holds
p is being_transposition
proofend;

theorem :: MATRIX_9:32
for p being Permutation of (Seg 3) st p = <*3,2,1*> holds
p is being_transposition
proofend;

theorem Th33: :: MATRIX_9:33
for n being Nat
for p being Permutation of (Seg n) st p = id (Seg n) holds
not p is being_transposition
proofend;

theorem Th34: :: MATRIX_9:34
for p being Permutation of (Seg 3) st p = <*3,1,2*> holds
not p is being_transposition
proofend;

theorem Th35: :: MATRIX_9:35
for p being Permutation of (Seg 3) st p = <*2,3,1*> holds
not p is being_transposition
proofend;

begin

theorem Th36: :: MATRIX_9:36
for n being Nat
for f being Permutation of (Seg n) holds f is FinSequence of Seg n
proofend;

theorem Th37: :: MATRIX_9:37
( <*2,1,3*> * <*1,3,2*> = <*2,3,1*> &amp; <*1,3,2*> * <*2,1,3*> = <*3,1,2*> &amp; <*2,1,3*> * <*3,2,1*> = <*3,1,2*> &amp; <*3,2,1*> * <*2,1,3*> = <*2,3,1*> &amp; <*3,2,1*> * <*3,2,1*> = <*1,2,3*> &amp; <*2,1,3*> * <*2,1,3*> = <*1,2,3*> &amp; <*1,3,2*> * <*1,3,2*> = <*1,2,3*> &amp; <*1,3,2*> * <*2,3,1*> = <*3,2,1*> &amp; <*2,3,1*> * <*2,3,1*> = <*3,1,2*> &amp; <*2,3,1*> * <*3,1,2*> = <*1,2,3*> &amp; <*3,1,2*> * <*2,3,1*> = <*1,2,3*> &amp; <*3,1,2*> * <*3,1,2*> = <*2,3,1*> &amp; <*1,3,2*> * <*3,2,1*> = <*2,3,1*> &amp; <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
proofend;

theorem Th38: :: MATRIX_9:38
for p being Permutation of (Seg 3) holds
( not p is being_transposition or p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
proofend;

theorem Th39: :: MATRIX_9:39
for n being Nat
for f, g being Element of Permutations n holds f * g in Permutations n
proofend;

Lm12:  <*1,2,3*> is even Permutation of (Seg 3)
by FINSEQ_2:53, MATRIX_2:25;

Lm13:  <*2,3,1*> is even Permutation of (Seg 3)
proofend;

Lm14:  <*3,1,2*> is even Permutation of (Seg 3)
proofend;

theorem :: MATRIX_9:40
for n being Nat
for l being FinSequence of (Group_of_Perm n) st (len l) mod 2 = 0 &amp; ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q &amp; q is being_transposition ) ) holds
Product l is even Permutation of (Seg n)
proofend;

Lm15:  for p being Permutation of (Seg 3) holds p * <*1,2,3*> = p
proofend;

Lm16:  for p being Permutation of (Seg 3) holds <*1,2,3*> * p = p
proofend;

theorem Th41: :: MATRIX_9:41
for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 &amp; ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q &amp; q is being_transposition ) ) &amp; not Product l = <*1,2,3*> &amp; not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
proofend;

Lm17:  for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 &amp; ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q &amp; q is being_transposition ) ) &amp; not Product l = <*1,2,3*> &amp; not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
proofend;

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

theorem Th42: :: MATRIX_9:42
<*3,2,1*> is odd Permutation of (Seg 3)
proofend;

theorem Th43: :: MATRIX_9:43
<*2,1,3*> is odd Permutation of (Seg 3)
proofend;

theorem Th44: :: MATRIX_9:44
<*1,3,2*> is odd Permutation of (Seg 3)
proofend;

theorem :: MATRIX_9:45
for p being odd Permutation of (Seg 3) holds
( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> )
proofend;

begin

theorem :: MATRIX_9:46
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
proofend;

theorem :: MATRIX_9:47
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
proofend;

theorem Th48: :: MATRIX_9:48
for i, n being Element of NAT
for p being Element of Permutations n st i in Seg n holds
ex k being Element of NAT st
( k in Seg n &amp; i = p . k )
proofend;

theorem Th49: :: MATRIX_9:49
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n &amp; (Path_matrix (p,M)) . l = 0. K )
proofend;

theorem Th50: :: MATRIX_9:50
for n being Nat
for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(Path_product M) . p = 0. K
proofend;

theorem Th51: :: MATRIX_9:51
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K
proofend;

theorem Th52: :: MATRIX_9:52
for n being Nat
for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(PPath_product M) . p = 0. K
proofend;

Lm18:  for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K
proofend;

theorem :: MATRIX_9:53
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
proofend;

theorem :: MATRIX_9:54
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Per M = 0. K by Lm18;

begin

theorem :: MATRIX_9:55
for n, i being Nat
for K being Field
for M, N being Matrix of n,K st i in Seg n holds
for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n &amp; i = p . k &amp; (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
proofend;

theorem :: MATRIX_9:56
for n being Nat
for K being Field
for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n &amp; ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) &amp; ( for l being Element of NAT st l <> i &amp; l in Seg n holds
Col (M,l) = Col (N,l) ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n &amp; (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
proofend;