:: by Ewa Romanowicz and Adam Grabowski

::

:: Received January 4, 2006

:: Copyright (c) 2006-2021 Association of Mizar Users

registration

let n be Nat;

existence

not for b_{1} being Element of Fin (Permutations n) holds b_{1} is empty

end;
existence

not for b

proof end;

scheme :: MATRIX_9:sch 1

NonEmptyFiniteX{ F_{1}() -> Element of NAT , F_{2}() -> non empty Element of Fin (Permutations F_{1}()), P_{1}[ set ] } :

provided

NonEmptyFiniteX{ F

provided

A1:
for x being Element of Permutations F_{1}() st x in F_{2}() holds

P_{1}[{x}]
and

A2: for x being Element of Permutations F_{1}()

for B being non empty Element of Fin (Permutations F_{1}()) st x in F_{2}() & B c= F_{2}() & not x in B & P_{1}[B] holds

P_{1}[B \/ {x}]

P

A2: for x being Element of Permutations F

for B being non empty Element of Fin (Permutations F

P

proof end;

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;

ex b_{1} being Function of (Seg n),(Seg n) st

( b_{1} is one-to-one & b_{1} is FinSequence-like )

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

( b

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))

f = Rev (id (Seg 2))

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

for f being FinSequence st n <> 0 & f in Permutations n holds

Rev f in Permutations n

proof end;

definition

let n be Nat;

let K be Field;

let M be Matrix of n,K;

ex b_{1} being Function of (Permutations n), the carrier of K st

for p being Element of Permutations n holds b_{1} . p = the multF of K $$ (Path_matrix (p,M))

for b_{1}, b_{2} being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b_{1} . p = the multF of K $$ (Path_matrix (p,M)) ) & ( for p being Element of Permutations n holds b_{2} . p = the multF of K $$ (Path_matrix (p,M)) ) holds

b_{1} = b_{2}

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

ex b

for p being Element of Permutations n holds b

proof end;

uniqueness for b

b

proof 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_{4} being Function of (Permutations n), the carrier of K holds

( b_{4} = PPath_product M iff for p being Element of Permutations n holds b_{4} . p = the multF of K $$ (Path_matrix (p,M)) );

for n being Nat

for K being Field

for M being Matrix of n,K

for b

( b

definition

let n be Nat;

let K be Field;

let M be Matrix of n,K;

the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) is Element of K ;

end;
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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M));

coherence the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M));

the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M)) is Element of K ;

:: 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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M));

for n being Nat

for K being Field

for M being Matrix of n,K holds Per M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M));

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*>

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*>

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;

registration

ex b_{1} being Permutation of (Seg 2) st b_{1} is odd
end;

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 b

proof end;

registration

let n be Nat;

ex b_{1} being Permutation of (Seg n) st b_{1} is even

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

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*>

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

for f, g being FinSequence st f ^ g in Permutations n holds

f ^ (Rev g) in Permutations n

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*>

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*>

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*>

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*>

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*>

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*>

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 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: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*> & <*1,2,3*> <> <*3,1,2*> )

by FINSEQ_1:78;

Lm7: ( <*3,2,1*> <> <*2,3,1*> & <*3,2,1*> <> <*3,1,2*> )

by FINSEQ_1:78;

Lm8: ( <*3,2,1*> <> <*2,1,3*> & <*1,3,2*> <> <*2,1,3*> )

by FINSEQ_1:78;

Lm9: ( <*1,3,2*> <> <*2,3,1*> & <*1,3,2*> <> <*3,1,2*> )

by FINSEQ_1:78;

Lm10: ( <*3,2,1*> <> <*1,3,2*> & <*2,3,1*> <> <*3,1,2*> )

by FINSEQ_1:78;

Lm11: ( <*2,3,1*> <> <*2,1,3*> & <*2,1,3*> <> <*3,1,2*> )

by FINSEQ_1:78;

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

for p being Permutation of (Seg n) st p = id (Seg n) holds

not p is being_transposition

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*> )

( not p is being_transposition or p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )

proof end;

Lm12: <*1,2,3*> is even Permutation of (Seg 3)

by FINSEQ_2:53, MATRIX_1:16;

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)

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*>

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

ex b_{1} being Permutation of (Seg 3) st b_{1} is odd
end;

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 b

proof end;

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)

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)

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 )

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 )

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

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 $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) = 0. K

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 $$ ((In ((Permutations n),(Fin (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

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 $$ ((In ((Permutations n),(Fin (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

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

theorem :: MATRIX_9:55

for i, n 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 )

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) )

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;