let n be Nat; :: thesis: for K being commutative Ring
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)
let K be commutative Ring; :: 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 = In ((Permutations n),(Fin (Permutations n)));
set I = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product (A @)));
A1: Det A = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product A)) by MATRIX_3:def 9;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A2: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;
A3: { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } c= In ((Permutations n),(Fin (Permutations n)))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } or z in In ((Permutations n),(Fin (Permutations n))) )
assume z in { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } ; :: thesis: z in In ((Permutations n),(Fin (Permutations n)))
then ex p being Permutation of (Seg n) st
( z = p " & p in In ((Permutations n),(Fin (Permutations n))) ) ;
hence z in In ((Permutations n),(Fin (Permutations n))) by A2, MATRIX_1:def 12; :: thesis: verum
end;
A4: In ((Permutations n),(Fin (Permutations n))) c= { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in In ((Permutations n),(Fin (Permutations n))) or z in { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } )
assume z in In ((Permutations n),(Fin (Permutations n))) ; :: thesis: z in { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) }
then reconsider q2 = z as Permutation of (Seg n) by A2, MATRIX_1:def 12;
set q3 = q2 " ;
( (q2 ") " = q2 & q2 " in In ((Permutations n),(Fin (Permutations n))) ) by A2, FUNCT_1:43, MATRIX_1:def 12;
hence z in { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } ; :: thesis: verum
end;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A5: ( In ((Permutations n),(Fin (Permutations n))) <> {} or the addF of K is having_a_unity ) by SUBSET_1:def 8;
then consider G0 being Function of (Fin (Permutations n)), the carrier of K such that
A6: the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product (A @))) = G0 . (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (A @)) . x)) by SETWISEO:def 3;
deffunc H1( 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
H1(x2) in the carrier of K
proof
let x2 be set ; :: thesis: ( x2 in Fin (Permutations n) implies H1(x2) in the carrier of K )
assume x2 in Fin (Permutations n) ; :: thesis: H1(x2) in the carrier of K
{ (p ") where p is Permutation of (Seg n) : p in x2 } c= Permutations n
proof
let r be object ; :: 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_1:def 12; :: thesis: verum
end;
then { (p ") where p is Permutation of (Seg n) : p in x2 } is Element of Fin (Permutations n) by FINSUB_1:17;
hence H1(x2) in the carrier of K by FUNCT_2:5; :: 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 = H1(x5) from FUNCT_2:sch 11(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_1:def 12;
A14: q " is Element of Permutations n by MATRIX_1:def 12;
A15: { (p ") where p is Permutation of (Seg n) : p in B4 } c= {(q ")}
proof
let z be object ; :: 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 object ; :: 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;
then G1 . B4 = G0 . {(q ")} by A11
.= (Path_product (A @)) . (q ") by A8, A14
.= (Path_product A) . q by A12, Th35 ;
hence G1 . {x} = (Path_product A) . x ; :: thesis: verum
end;
A18: for B9 being Element of Fin (Permutations n) st B9 c= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} implies for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x)) )
assume that
A19: B9 c= In ((Permutations n),(Fin (Permutations n))) and
A20: B9 <> {} ; :: thesis: for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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 (In ((Permutations n),(Fin (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 object ; :: 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_1:def 12; :: 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:17;
set d = the Element of B9;
let x be Element of Permutations n; :: thesis: ( x in (In ((Permutations n),(Fin (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_1:def 12;
reconsider y = px " as Element of Permutations n by MATRIX_1:def 12;
A21: B2 \/ {y} c= { (p ") where p is Permutation of (Seg n) : p in B9 \/ {x} }
proof
let z be object ; :: 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 :: thesis: ( ( z in B2 & z in { (p ") where p is Permutation of (Seg n) : p in B9 \/ {x} } ) or ( z = y & z in { (p ") where p is Permutation of (Seg n) : p in B9 \/ {x} } ) )
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= In ((Permutations n),(Fin (Permutations n)))
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in B2 or u in In ((Permutations n),(Fin (Permutations n))) )
assume u in B2 ; :: thesis: u in In ((Permutations n),(Fin (Permutations n)))
then ex p being Permutation of (Seg n) st
( p " = u & p in B9 ) ;
hence u in In ((Permutations n),(Fin (Permutations n))) by A2, MATRIX_1:def 12; :: thesis: verum
end;
assume x in (In ((Permutations n),(Fin (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 :: thesis: not y in B2
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:43;
hence contradiction by A27, A29, FUNCT_1:43; :: thesis: verum
end;
then A30: y in (In ((Permutations n),(Fin (Permutations n)))) \ B2 by A2, XBOOLE_0:def 5;
the Element of B9 in In ((Permutations n),(Fin (Permutations n))) by A19, A20;
then reconsider pd = the Element of B9 as Permutation of (Seg n) by A2, MATRIX_1:def 12;
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 object ; :: 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 :: thesis: ( ( p in B9 & ( z in B2 or z in {y} ) ) or ( p in {x} & ( z in B2 or z in {y} ) ) )
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;
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, Th35; :: 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:1;
then reconsider B3 = {} as Element of Fin (Permutations n) by FINSUB_1:17;
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 object ; :: 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 . (In ((Permutations n),(Fin (Permutations n)))) = G0 . { (p ") where p is Permutation of (Seg n) : p in In ((Permutations n),(Fin (Permutations n))) } by A11;
then the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product (A @))) = G1 . (In ((Permutations n),(Fin (Permutations n)))) by A6, A3, A4, XBOOLE_0:def 10;
then the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product A)) = the addF of K $$ ((In ((Permutations n),(Fin (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