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


begin

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

registration
let n be Nat;
cluster non empty finite Element of Fin (Permutations n);
existence
not for b1 being Element of Fin (Permutations n) holds b1 is empty
proof end;
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}]
proof end;

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

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 quasi_total finite FinSequence-like Element of bool [:(Seg n),(Seg n):];
existence
ex b1 being Function of (Seg n),(Seg n) st
( b1 is one-to-one & b1 is FinSequence-like )
proof end;
end;

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

theorem Th2: :: MATRIX_9:2
( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 )
proof end;

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

begin

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

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

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

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))
proof end;
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)) ) & ( for p being Element of Permutations n holds b2 . p = the multF of K $$ (Path_matrix (p,M)) ) holds
b1 = b2
proof end;
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
proof end;

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

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

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

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

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 Element of bool [:(Seg 2),(Seg 2):];
existence
not for b1 being Permutation of (Seg 2) holds b1 is even
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

begin

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

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

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

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

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

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

begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 & i = p . k )
proof end;

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 & ( 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 & (Path_matrix (p,M)) . l = 0. K )
proof end;

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

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

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

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

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 & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
proof end;

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 & ( 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 & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
proof end;

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 & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & 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 & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
proof end;