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 @ ) )
assume A1: n >= 1 ; :: thesis: 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);
A2: ( FinOmega (Permutations n) <> {} or the addF of K is having_a_unity ) by MATRIX_2:30, MATRIX_2:def 17;
A3: FinOmega (Permutations n) = Permutations n by MATRIX_2:30, MATRIX_2:def 17;
set I = the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ ));
consider G0 being Function of (Fin (Permutations n)),the carrier of K such that
A4: ( the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) = G0 . (FinOmega (Permutations n)) & ( for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e ) & ( for x being Element of Permutations n holds G0 . {x} = (Path_product (A @ )) . x ) & ( for B' being Element of Fin (Permutations n) st B' c= FinOmega (Permutations n) & B' <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B' holds
G0 . (B' \/ {x}) = the addF of K . (G0 . B'),((Path_product (A @ )) . x) ) ) by A2, SETWISEO:def 3;
deffunc H₁( set ) -> set = G0 . { (p " ) where p is Permutation of (Seg n) : p in $1 } ;
A5: 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 consider p being Permutation of (Seg n) such that
A6: ( r = p " & p in x2 ) ;
thus r in Permutations n by A6, 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
A7: for x5 being set st x5 in Fin (Permutations n) holds
G1 . x5 = H₁(x5) from FUNCT_2:sch 2(A5);
A8: the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) = G1 . (FinOmega (Permutations n))

proof

A9: G1 . (FinOmega (Permutations n)) = G0 . { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } by A7;
A10: { (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 consider p being Permutation of (Seg n) such that
A11: ( z = p " & p in FinOmega (Permutations n) ) ;
thus z in FinOmega (Permutations n) by A3, A11, MATRIX_2:def 11; :: thesis: verum

end;

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 A3, MATRIX_2:def 11;
set q3 = q2 " ;
A12: (q2 " ) " = q2 by FUNCT_1:65;
q2 " in FinOmega (Permutations n) by A3, MATRIX_2:def 11;
hence z in { (p " ) where p is Permutation of (Seg n) : p in FinOmega (Permutations n) } by A12; :: thesis: verum

end;

hence the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) = G1 . (FinOmega (Permutations n)) by A4, A9, A10, XBOOLE_0:def 10; :: thesis: verum

end;

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

proof

let e be Element of the carrier of K; :: thesis: ( e is_a_unity_wrt the addF of K implies G1 . {} = e )
assume A14: e is_a_unity_wrt the addF of K ; :: thesis: G1 . {} = e
{} 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;
{ (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 consider p being Permutation of (Seg n) such that
A15: ( s = p " & p in B3 ) ;
thus s in {} by A15; :: thesis: verum

end;

then { (p " ) where p is Permutation of (Seg n) : p in B3 } = {} ;
then G0 . { (p " ) where p is Permutation of (Seg n) : p in B3 } = e by A4, A14;
hence G1 . {} = e by A7; :: thesis: verum

end;

A16: 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;
A17: q " is Element of Permutations n by MATRIX_2:def 11;
{ (p " ) where p is Permutation of (Seg n) : p in B4 } = {(q " )}

proof

A18: { (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
A19: ( z = p " & p in B4 ) ;
p = x by A19, TARSKI:def 1;
hence z in {(q " )} by A19, 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 A20: z in {(q " )} ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B4 }
A21: q in B4 by TARSKI:def 1;
z = q " by A20, TARSKI:def 1;
hence z in { (p " ) where p is Permutation of (Seg n) : p in B4 } by A21; :: thesis: verum

end;

hence { (p " ) where p is Permutation of (Seg n) : p in B4 } = {(q " )} by A18, XBOOLE_0:def 10; :: thesis: verum

end;

then G1 . B4 = G0 . {(q " )} by A7
.= (Path_product (A @ )) . (q " ) by A4, A17
.= (Path_product A) . q by A1, Th36 ;
hence G1 . {x} = (Path_product A) . x ; :: thesis: verum

end;

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

proof

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

proof

let x be Element of Permutations n; :: thesis: ( x in (FinOmega (Permutations n)) \ B' implies G1 . (B' \/ {x}) = the addF of K . (G1 . B'),((Path_product A) . x) )
assume x in (FinOmega (Permutations n)) \ B' ; :: thesis: G1 . (B' \/ {x}) = the addF of K . (G1 . B'),((Path_product A) . x)
then A23: ( x in FinOmega (Permutations n) & not x in B' ) by XBOOLE_0:def 5;
A24: G1 . (B' \/ {.x.}) = G0 . { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} } by A7;
{ (p " ) where p is Permutation of (Seg n) : p in B' } 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 B' } or v in Permutations n )
assume v in { (p " ) where p is Permutation of (Seg n) : p in B' } ; :: thesis: v in Permutations n
then consider p being Permutation of (Seg n) such that
A25: ( p " = v & p in B' ) ;
thus v in Permutations n by A25, MATRIX_2:def 11; :: thesis: verum

end;

then reconsider B2 = { (p " ) where p is Permutation of (Seg n) : p in B' } as Element of Fin (Permutations n) by FINSUB_1:34, MATRIX_2:30;
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;
A26: B2 \/ {y} = { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} }

proof

thus B2 \/ {y} c= { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} } :: according to XBOOLE_0:def 10 :: thesis: { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} } c= B2 \/ {y}

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 B' \/ {x} } )
assume z in B2 \/ {y} ; :: thesis: z in { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} }
then A27: ( z in B2 or z in {y} ) by XBOOLE_0:def 3;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

thus { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} } c= B2 \/ {y} :: thesis: verum

proof

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

now

per cases ( p in B' or p in {x} ) by A30, XBOOLE_0:def 3;

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

hence ( z in B2 or z in {y} ) by A30; :: 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 A30, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

end;

A31: 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 consider p being Permutation of (Seg n) such that
A32: ( p " = u & p in B' ) ;
thus u in FinOmega (Permutations n) by A3, A32, MATRIX_2:def 11; :: thesis: verum

end;

consider d being Element of B';
d in FinOmega (Permutations n) by A22, TARSKI:def 3;
then reconsider pd = d as Permutation of (Seg n) by A3, MATRIX_2:def 11;
A33: pd " in B2 by A22;

now

assume y in B2 ; :: thesis: contradiction
then consider pp being Permutation of (Seg n) such that
A34: ( y = pp " & pp in B' ) ;
px = (pp " ) " by A34, FUNCT_1:65;
hence contradiction by A23, A34, FUNCT_1:65; :: thesis: verum

end;

then y in (FinOmega (Permutations n)) \ B2 by A3, XBOOLE_0:def 5;
then A35: G0 . { (p " ) where p is Permutation of (Seg n) : p in B' \/ {x} } = the addF of K . (G0 . B2),((Path_product (A @ )) . y) by A4, A26, A31, A33;
G0 . B2 = G1 . B' by A7;
hence G1 . (B' \/ {x}) = the addF of K . (G1 . B'),((Path_product A) . x) by A1, A24, A35, Th36; :: thesis: verum

end;

end;

then A36: the addF of K $$ (FinOmega (Permutations n)),(Path_product A) = the addF of K $$ (FinOmega (Permutations n)),(Path_product (A @ )) by A2, A8, A13, A16, SETWISEO:def 3;
Det A = the addF of K $$ (FinOmega (Permutations n)),(Path_product A) by MATRIX_3:def 9;
hence Det A = Det (A @ ) by A36, MATRIX_3:def 9; :: thesis: verum