:: Determinant of Some Matrices of Field Elements
:: by Yatsuka Nakamura
::
:: Received January 4, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: MATRIX_7:1
for f being Permutation of (Seg 2) holds
( f = <*1,2*> or f = <*2,1*> )
proofend;

theorem Th2: :: MATRIX_7:2
for f being FinSequence st ( f = <*1,2*> or f = <*2,1*> ) holds
f is Permutation of (Seg 2)
proofend;

theorem Th3: :: MATRIX_7:3
Permutations 2 = {<*1,2*>,<*2,1*>}
proofend;

theorem Th4: :: MATRIX_7:4
for p being Permutation of (Seg 2) st p is being_transposition holds
p = <*2,1*>
proofend;

theorem Th5: :: MATRIX_7:5
for D being non empty set
for f being FinSequence of D
for k2 being Element of NAT st 1 <= k2 &amp; k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
proofend;

theorem Th6: :: MATRIX_7:6
for D being non empty set
for f being FinSequence of D st 2 <= len f holds
f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
proofend;

theorem Th7: :: MATRIX_7:7
for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
proofend;

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

theorem Th8: :: MATRIX_7:8
for a being Element of (Group_of_Perm 2) st ex q being Element of Permutations 2 st
( q = a &amp; q is being_transposition ) holds
a = <*2,1*>
proofend;

theorem :: MATRIX_7:9
for n being Element of NAT
for a, b being Element of (Group_of_Perm n)
for pa, pb being Element of Permutations n st a = pa &amp; b = pb holds
a * b = pb * pa by MATRIX_2:def_10;

theorem Th10: :: MATRIX_7:10
for a, b being Element of (Group_of_Perm 2) st ex p being Element of Permutations 2 st
( p = a &amp; p is being_transposition ) &amp; ex q being Element of Permutations 2 st
( q = b &amp; q is being_transposition ) holds
a * b = <*1,2*>
proofend;

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

theorem :: MATRIX_7:12
for K being Field
for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
proofend;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
let a be Element of K;
:: original:*
redefine funca * M ->  Matrix of n,K;
coherence
 a * M is Matrix of n,K
proofend;
end;

theorem Th13: :: MATRIX_7:13
for K being Field
for n, m being Element of NAT holds
( len (0. (K,n,m)) = n &amp; dom (0. (K,n,m)) = Seg n )
proofend;

theorem Th14: :: MATRIX_7:14
for K being Field
for n being Element of NAT
for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
proofend;

theorem :: MATRIX_7:15
for K being Field
for n being Element of NAT st n >= 1 holds
Det (0. (K,n,n)) = 0. K
proofend;

definition
let x, y, a, b be set ;
func IFIN (x,y,a,b) ->  set  equals :Def1: :: MATRIX_7:def 1
a if x in y
otherwise b;
correctness
coherence
( ( x in y implies a is set ) &amp; ( not x in y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines IFIN MATRIX_7:def_1_:_
 for x, y, a, b being set holds
( ( x in y implies IFIN (x,y,a,b) = a ) &amp; ( not x in y implies IFIN (x,y,a,b) = b ) );

theorem :: MATRIX_7:16
for K being Field
for n being Element of NAT st n >= 1 holds
Det (1. (K,n)) = 1_ K
proofend;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
:: original:diagonal
redefine attrM is diagonal  means :Def2: :: MATRIX_7:def 2
 for i, j being Element of NAT st i in Seg n &amp; j in Seg n &amp; i <> j holds
M * (i,j) = 0. K;
compatibility
 ( M is diagonal iff for i, j being Element of NAT st i in Seg n &amp; j in Seg n &amp; i <> j holds
M * (i,j) = 0. K )
proofend;
end;

:: deftheorem Def2 defines diagonal MATRIX_7:def_2_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is diagonal iff for i, j being Element of NAT st i in Seg n &amp; j in Seg n &amp; i <> j holds
M * (i,j) = 0. K );

theorem :: MATRIX_7:17
for K being Field
for n being Element of NAT
for A being Matrix of n,K st n >= 1 &amp; A is V164(b1) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
proofend;

theorem Th18: :: MATRIX_7:18
for n being Nat
for p being Element of Permutations n holds p " is Element of Permutations n
proofend;

definition
let n be Nat;
let p be Element of Permutations n;
:: original:"
redefine funcp "  ->  Element of Permutations n;
coherence
 p " is Element of Permutations n by Th18;
end;

theorem Th19: :: MATRIX_7:19
for n being Nat
for K being Field
for A being Matrix of n,K holds A @ is Matrix of n,K ;

theorem :: MATRIX_7:20
for G being Group
for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
proofend;

definition
let G be Group;
let f be FinSequence of G;
canceled;
funcf "  ->  FinSequence of G means :Def4: :: MATRIX_7:def 4
( len it = len f &amp; ( for i being Element of NAT st i in dom f holds
it /. i = (f /. i) " ) );
existence
 ex b1 being FinSequence of G st
( len b1 = len f &amp; ( for i being Element of NAT st i in dom f holds
b1 /. i = (f /. i) " ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of G st len b1 = len f &amp; ( for i being Element of NAT st i in dom f holds
b1 /. i = (f /. i) " ) &amp; len b2 = len f &amp; ( for i being Element of NAT st i in dom f holds
b2 /. i = (f /. i) " ) holds
b1 = b2
proofend;
end;

:: deftheorem  MATRIX_7:def_3_:_
canceled;

:: deftheorem Def4 defines " MATRIX_7:def_4_:_
 for G being Group
for f, b3 being FinSequence of G holds
( b3 = f " iff ( len b3 = len f &amp; ( for i being Element of NAT st i in dom f holds
b3 /. i = (f /. i) " ) ) );

theorem Th21: :: MATRIX_7:21
for G being Group holds (<*> the carrier of G) " = <*> the carrier of G
proofend;

theorem Th22: :: MATRIX_7:22
for G being Group
for f, g being FinSequence of G holds (f ^ g) " = (f ") ^ (g ")
proofend;

theorem Th23: :: MATRIX_7:23
for G being Group
for a being Element of G holds <*a*> " = <*(a ")*>
proofend;

theorem Th24: :: MATRIX_7:24
for G being Group
for f being FinSequence of G holds Product (f ^ ((Rev f) ")) = 1_ G
proofend;

theorem Th25: :: MATRIX_7:25
for G being Group
for f being FinSequence of G holds Product (((Rev f) ") ^ f) = 1_ G
proofend;

theorem Th26: :: MATRIX_7:26
for G being Group
for f being FinSequence of G holds (Product f) " = Product ((Rev f) ")
proofend;

theorem Th27: :: MATRIX_7:27
for n being Nat
for ITP being Element of Permutations n
for ITG being Element of (Group_of_Perm n) st ITG = ITP &amp; n >= 1 holds
ITP " = ITG "
proofend;

Lm2:  for n being Element of NAT
for IT being Element of Permutations n st IT is even &amp; n >= 1 holds
IT " is even
proofend;

theorem Th28: :: MATRIX_7:28
for n being Element of NAT
for IT being Element of Permutations n st n >= 1 holds
( IT is even iff IT " is even )
proofend;

theorem Th29: :: MATRIX_7:29
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
proofend;

theorem :: MATRIX_7:30
for K being Field
for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = ( the multF of K $$ f1) * ( the multF of K $$ f2) by FINSOP_1:5;

theorem Th31: :: MATRIX_7:31
for K being Field
for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
the multF of K $$ R1 = the multF of K $$ R2
proofend;

theorem Th32: :: MATRIX_7:32
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st len f = n &amp; g = f * p holds
f,g are_fiberwise_equipotent
proofend;

theorem :: MATRIX_7:33
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st n >= 1 &amp; len f = n &amp; g = f * p holds
the multF of K $$ f = the multF of K $$ g by Th31, Th32;

theorem Th34: :: MATRIX_7:34
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f being FinSequence of K st n >= 1 &amp; len f = n holds
f * p is FinSequence of K
proofend;

theorem Th35: :: MATRIX_7:35
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
proofend;

theorem Th36: :: MATRIX_7:36
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
proofend;

theorem :: MATRIX_7:37
for n being Element of NAT
for K being Field
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)
proofend;