let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @ )
let K be Field; :: thesis: for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @ )
let A be Matrix of n,K; :: thesis: ( n >= 1 implies Det A = Det (A @ ) )
set f = Path_product A;
set f2 = Path_product (A @ );
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
set B = FinOmega (Permutations n);
set I = the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ ));
A1: Det A = the addF of K $$ (FinOmega (Permutations n)),(Path_product A) by MATRIX_3:def 9;
A2: FinOmega (Permutations n) = Permutations n by MATRIX_2:30, MATRIX_2:def 17;
A3: { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } c= FinOmega (Permutations n)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } or z in FinOmega (Permutations n) )
assume z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } ; :: thesis: z in FinOmega (Permutations n)
then ex p being Permutation of (Seg n) st
( z = p " & p in FinOmega (Permutations n) ) ;
hence z in FinOmega (Permutations n) by A2, MATRIX_2:def 11; :: thesis: verum

end;

A4: FinOmega (Permutations n) c= { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in FinOmega (Permutations n) or z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } )
assume z in FinOmega (Permutations n) ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) }
then reconsider q2 = z as Permutation of (Seg n) by A2, MATRIX_2:def 11;
set q3 = q2 " ;
( (q2 " ) " = q2 & q2 " in FinOmega (Permutations n) ) by A2, FUNCT_1:65, MATRIX_2:def 11;
hence z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } ; :: thesis: verum

end;

A5: ( FinOmega (Permutations n) <> {} or the addF of K is having_a_unity ) by MATRIX_2:30, MATRIX_2:def 17;
then consider G0 being Function of (Fin (Permutations n)),the carrier of K such that
A6: the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) = G0 . (FinOmega (Permutations n)) and
A7: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e and
A8: for x being Element of Permutations n holds G0 . {x} = (Path_product (A @ )) . x and
A9: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . (G0 . B9),((Path_product (A @ )) . x) by SETWISEO:def 3;
deffunc H₁( set ) -> set = G0 . { (p " ) where p is Permutation of (Seg n) : p in $1 } ;
A10: for x2 being set st x2 in Fin (Permutations n) holds
H₁(x2) in the carrier of K

proof

let x2 be set ; :: thesis: ( x2 in Fin (Permutations n) implies H₁(x2) in the carrier of K )
assume x2 in Fin (Permutations n) ; :: thesis: H₁(x2) in the carrier of K
{ (p " ) where p is Permutation of (Seg n) : p in x2 } c= Permutations n

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in { (p " ) where p is Permutation of (Seg n) : p in x2 } or r in Permutations n )
assume r in { (p " ) where p is Permutation of (Seg n) : p in x2 } ; :: thesis: r in Permutations n
then ex p being Permutation of (Seg n) st
( r = p " & p in x2 ) ;
hence r in Permutations n by MATRIX_2:def 11; :: thesis: verum

end;

then { (p " ) where p is Permutation of (Seg n) : p in x2 } is Finite_Subset of (Permutations n) by FINSUB_1:34, MATRIX_2:30;
hence H₁(x2) in the carrier of K by FUNCT_2:7; :: thesis: verum

end;

consider G1 being Function of (Fin (Permutations n)),the carrier of K such that
A11: for x5 being set st x5 in Fin (Permutations n) holds
G1 . x5 = H₁(x5) from FUNCT_2:sch 2(A10);
assume A12: n >= 1 ; :: thesis: Det A = Det (A @ )
A13: for x being Element of Permutations n holds G1 . {x} = (Path_product A) . x

proof

let x be Element of Permutations n; :: thesis: G1 . {x} = (Path_product A) . x
reconsider B4 = {.x.} as Element of Fin (Permutations n) ;
reconsider q = x as Permutation of (Seg n) by MATRIX_2:def 11;
A14: q " is Element of Permutations n by MATRIX_2:def 11;
A15: { (p " ) where p is Permutation of (Seg n) : p in B4 } c= {(q " )}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (p " ) where p is Permutation of (Seg n) : p in B4 } or z in {(q " )} )
assume z in { (p " ) where p is Permutation of (Seg n) : p in B4 } ; :: thesis: z in {(q " )}
then consider p being Permutation of (Seg n) such that
A16: z = p " and
A17: p in B4 ;
p = x by A17, TARSKI:def 1;
hence z in {(q " )} by A16, TARSKI:def 1; :: thesis: verum

end;

{(q " )} c= { (p " ) where p is Permutation of (Seg n) : p in B4 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {(q " )} or z in { (p " ) where p is Permutation of (Seg n) : p in B4 } )
assume z in {(q " )} ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B4 }
then ( q in B4 & z = q " ) by TARSKI:def 1;
hence z in { (p " ) where p is Permutation of (Seg n) : p in B4 } ; :: thesis: verum

end;

then { (p " ) where p is Permutation of (Seg n) : p in B4 } = {(q " )} by A15, XBOOLE_0:def 10;
then G1 . B4 = G0 . {(q " )} by A11
.= (Path_product (A @ )) . (q " ) by A8, A14
.= (Path_product A) . q by A12, Th36 ;
hence G1 . {x} = (Path_product A) . x ; :: thesis: verum

end;

A18: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x)

proof

let B9 be Element of Fin (Permutations n); :: thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x) )
assume that
A19: B9 c= FinOmega (Permutations n) and
A20: B9 <> {} ; :: thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x)
thus for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x) :: thesis: verum

proof

{ (p " ) where p is Permutation of (Seg n) : p in B9 } c= Permutations n

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { (p " ) where p is Permutation of (Seg n) : p in B9 } or v in Permutations n )
assume v in { (p " ) where p is Permutation of (Seg n) : p in B9 } ; :: thesis: v in Permutations n
then ex p being Permutation of (Seg n) st
( p " = v & p in B9 ) ;
hence v in Permutations n by MATRIX_2:def 11; :: thesis: verum

end;

then reconsider B2 = { (p " ) where p is Permutation of (Seg n) : p in B9 } as Element of Fin (Permutations n) by FINSUB_1:34, MATRIX_2:30;
consider d being Element of B9;
let x be Element of Permutations n; :: thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x) )
reconsider px = x as Permutation of (Seg n) by MATRIX_2:def 11;
reconsider y = px " as Element of Permutations n by MATRIX_2:def 11;
A21: B2 \/ {y} c= { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in B2 \/ {y} or z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } )
assume z in B2 \/ {y} ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} }
then A22: ( z in B2 or z in {y} ) by XBOOLE_0:def 3;

now

per cases ( z in B2 or z = y ) by A22, TARSKI:def 1;

case z in B2 ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} }

then consider p being Permutation of (Seg n) such that
A23: z = p " and
A24: p in B9 ;
p in B9 \/ {x} by A24, XBOOLE_0:def 3;
hence z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } by A23; :: thesis: verum

end;

case A25: z = y ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} }

px in {x} by TARSKI:def 1;
then px in B9 \/ {x} by XBOOLE_0:def 3;
hence z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } by A25; :: thesis: verum

end;

end;

end;

hence z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } ; :: thesis: verum

end;

A26: B2 c= FinOmega (Permutations n)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in B2 or u in FinOmega (Permutations n) )
assume u in B2 ; :: thesis: u in FinOmega (Permutations n)
then ex p being Permutation of (Seg n) st
( p " = u & p in B9 ) ;
hence u in FinOmega (Permutations n) by A2, MATRIX_2:def 11; :: thesis: verum

end;

assume x in (FinOmega (Permutations n)) \ B9 ; :: thesis: G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x)
then A27: not x in B9 by XBOOLE_0:def 5;

now

assume y in B2 ; :: thesis: contradiction
then consider pp being Permutation of (Seg n) such that
A28: y = pp " and
A29: pp in B9 ;
px = (pp " ) " by A28, FUNCT_1:65;
hence contradiction by A27, A29, FUNCT_1:65; :: thesis: verum

end;

then A30: y in (FinOmega (Permutations n)) \ B2 by A2, XBOOLE_0:def 5;
d in FinOmega (Permutations n) by A19, A20, TARSKI:def 3;
then reconsider pd = d as Permutation of (Seg n) by A2, MATRIX_2:def 11;
A31: pd " in B2 by A20;
A32: ( G1 . (B9 \/ {.x.}) = G0 . { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } & G0 . B2 = G1 . B9 ) by A11;
{ (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } c= B2 \/ {y}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } or z in B2 \/ {y} )
assume z in { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } ; :: thesis: z in B2 \/ {y}
then consider p being Permutation of (Seg n) such that
A33: z = p " and
A34: p in B9 \/ {x} ;

now

per cases ( p in B9 or p in {x} ) by A34, XBOOLE_0:def 3;

case p in B9 ; :: thesis: ( z in B2 or z in {y} )

hence ( z in B2 or z in {y} ) by A33; :: thesis: verum

end;

case p in {x} ; :: thesis: ( z in B2 or z in {y} )

then p = x by TARSKI:def 1;
hence ( z in B2 or z in {y} ) by A33, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence z in B2 \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

then B2 \/ {y} = { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } by A21, XBOOLE_0:def 10;
then G0 . { (p " ) where p is Permutation of (Seg n) : p in B9 \/ {x} } = the addF of K . (G0 . B2),((Path_product (A @ )) . y) by A9, A26, A31, A30;
hence G1 . (B9 \/ {x}) = the addF of K . (G1 . B9),((Path_product A) . x) by A12, A32, Th36; :: thesis: verum

end;

end;

A35: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G1 . {} = e

proof

{} is Subset of (Permutations n) by SUBSET_1:4;
then reconsider B3 = {} as Element of Fin (Permutations n) by FINSUB_1:34, MATRIX_2:30;
let e be Element of the carrier of K; :: thesis: ( e is_a_unity_wrt the addF of K implies G1 . {} = e )
{ (p " ) where p is Permutation of (Seg n) : p in B3 } c= {}

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { (p " ) where p is Permutation of (Seg n) : p in B3 } or s in {} )
assume s in { (p " ) where p is Permutation of (Seg n) : p in B3 } ; :: thesis: s in {}
then ex p being Permutation of (Seg n) st
( s = p " & p in B3 ) ;
hence s in {} ; :: thesis: verum

end;

then A36: { (p " ) where p is Permutation of (Seg n) : p in B3 } = {} ;
assume e is_a_unity_wrt the addF of K ; :: thesis: G1 . {} = e
then G0 . { (p " ) where p is Permutation of (Seg n) : p in B3 } = e by A7, A36;
hence G1 . {} = e by A11; :: thesis: verum

end;

G1 . (FinOmega (Permutations n)) = G0 . { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } by A11;
then the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) = G1 . (FinOmega (Permutations n)) by A6, A3, A4, XBOOLE_0:def 10;
then the addF of K $$ (FinOmega (Permutations n)),(Path_product A) = the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) by A5, A35, A13, A18, SETWISEO:def 3;
hence Det A = Det (A @ ) by A1, MATRIX_3:def 9; :: thesis: verum