:: 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 b₁ being Element of Fin (Permutations n) holds b₁ is empty

proof end;

end;

scheme :: MATRIX_9:sch 1
NonEmptyFiniteX{ F₁() -> Element of NAT , F₂() -> non empty Element of Fin (Permutations F₁()), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x being Element of Permutations F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of Permutations F₁()
for B being non empty Element of Fin (Permutations F₁()) st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[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 b₁ being Function of (Seg n),(Seg n) st
( b₁ is one-to-one & b₁ 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 b₁ being Function of (Permutations n), the carrier of K st
for p being Element of Permutations n holds b₁ . p = the multF of K $$ (Path_matrix (p,M))

proof end;

uniqueness
for b₁, b₂ being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b₁ . p = the multF of K $$ (Path_matrix (p,M)) ) & ( for p being Element of Permutations n holds b₂ . p = the multF of K $$ (Path_matrix (p,M)) ) holds
b₁ = b₂

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 b₄ being Function of (Permutations n), the carrier of K holds
( b₄ = PPath_product M iff for p being Element of Permutations n holds b₄ . 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 b₁ being Permutation of (Seg 2) holds b₁ 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 b₁ being Permutation of (Seg n) st b₁ 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 b₁ being Permutation of (Seg 3) holds b₁ 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;