let n be Nat; :: thesis: for K being Field
for A, B being Matrix of n, st 0 < n holds
Det (A * B) = (Det A) * (Det B)
let K be Field; :: thesis: for A, B being Matrix of n, st 0 < n holds
Det (A * B) = (Det A) * (Det B)
let A, B be Matrix of n,; :: thesis: ( 0 < n implies Det (A * B) = (Det A) * (Det B) )
assume A1: 0 < n ; :: thesis: Det (A * B) = (Det A) * (Det B)
set P = Permutations n;
set KK = the carrier of K;
set mm = the multF of K;
set aa = the addF of K;
set AB = A * B;
consider SUM being Function of Permutations n,the carrier of K such that
A2: Det (A * B) = the addF of K $$ (FinOmega (Permutations n)),SUM and
A3: for perm being Element of Permutations n holds SUM . perm = (the multF of K $$ (Path_matrix perm,A)) * (- (Det B),perm) by A1, Th61;
set Path = Path_product A;
set F = FinOmega (Permutations n);
A4: FinOmega (Permutations n) = Permutations n by MATRIX_2:30, MATRIX_2:def 17;
then consider Ga being Function of Fin (Permutations n),the carrier of K such that
A5: Det A = Ga . (FinOmega (Permutations n)) and
A6: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
Ga . {} = e and
A7: for x being Element of Permutations n holds Ga . {x} = (Path_product A) . x and
A8: 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
Ga . (B' \/ {x}) = the addF of K . (Ga . B'),((Path_product A) . x) by SETWISEO:def 3;
A9: Ga . {} = 0. K by A6, FVSUM_1:8;
consider Gs being Function of Fin (Permutations n),the carrier of K such that
A10: Det (A * B) = Gs . (FinOmega (Permutations n)) and
A11: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
Gs . {} = e and
A12: for x being Element of Permutations n holds Gs . {x} = SUM . x and
A13: 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
Gs . (B' \/ {x}) = the addF of K . (Gs . B'),(SUM . x) by A2, A4, SETWISEO:def 3;
defpred S₁[ set ] means for B' being Element of Fin (Permutations n) st B' = $1 holds
Gs . B' = (Ga . B') * (Det B);
A14: for B' being Element of Fin (Permutations n)
for b being Element of Permutations n st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]

proof

let B' be Element of Fin (Permutations n); :: thesis: for b being Element of Permutations n st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]
let b be Element of Permutations n; :: thesis: ( S₁[B'] & not b in B' implies S₁[B' \/ {b}] )
assume that
A15: S₁[B'] and
A16: not b in B' ; :: thesis: S₁[B' \/ {b}]
set mA = the multF of K $$ (Path_matrix b,A);
let Bb be Element of Fin (Permutations n); :: thesis: ( Bb = B' \/ {b} implies Gs . Bb = (Ga . Bb) * (Det B) )
assume A17: Bb = B' \/ {b} ; :: thesis: Gs . Bb = (Ga . Bb) * (Det B)

A18: now

per cases ( b is even or not b is even ) ;

suppose A19: b is even ; :: thesis: SUM . b = ((Path_product A) . b) * (Det B)

then A20: - (the multF of K $$ (Path_matrix b,A)),b = the multF of K $$ (Path_matrix b,A) by MATRIX_2:def 16;
- (Det B),b = Det B by A19, MATRIX_2:def 16;
hence SUM . b = (- (the multF of K $$ (Path_matrix b,A)),b) * (Det B) by A3, A20
.= ((Path_product A) . b) * (Det B) by MATRIX_3:def 8 ;
:: thesis: verum

end;

suppose A21: not b is even ; :: thesis: SUM . b = ((Path_product A) . b) * (Det B)

then A22: - (the multF of K $$ (Path_matrix b,A)),b = - (the multF of K $$ (Path_matrix b,A)) by MATRIX_2:def 16;
- (Det B),b = - (Det B) by A21, MATRIX_2:def 16;
then - ((- (the multF of K $$ (Path_matrix b,A)),b) * (Det B)) = (- (the multF of K $$ (Path_matrix b,A))) * (- (Det B),b) by A22, VECTSP_1:41
.= - ((the multF of K $$ (Path_matrix b,A)) * (- (Det B),b)) by VECTSP_1:41 ;
then ((the multF of K $$ (Path_matrix b,A)) * (- (Det B),b)) - ((- (the multF of K $$ (Path_matrix b,A)),b) * (Det B)) = 0. K by VECTSP_1:63;
then A23: (- (the multF of K $$ (Path_matrix b,A)),b) * (Det B) = (the multF of K $$ (Path_matrix b,A)) * (- (Det B),b) by VECTSP_1:66;
- (the multF of K $$ (Path_matrix b,A)),b = (Path_product A) . b by MATRIX_3:def 8;
hence SUM . b = ((Path_product A) . b) * (Det B) by A3, A23; :: thesis: verum

end;

end;

end;

per cases ( B' = {} or B' <> {} ) ;

suppose A24: B' = {} ; :: thesis: Gs . Bb = (Ga . Bb) * (Det B)

then Ga . Bb = (Path_product A) . b by A7, A17;
hence Gs . Bb = (Ga . Bb) * (Det B) by A12, A17, A18, A24; :: thesis: verum

end;

suppose A25: B' <> {} ; :: thesis: Gs . Bb = (Ga . Bb) * (Det B)

A26: B' c= Permutations n by FINSUB_1:def 5;
A27: b in (FinOmega (Permutations n)) \ B' by A4, A16, XBOOLE_0:def 5;
then Gs . Bb = the addF of K . (Gs . B'),(SUM . b) by A4, A13, A17, A25, A26;
then A28: Gs . Bb = ((Ga . B') * (Det B)) + (((Path_product A) . b) * (Det B)) by A15, A18;
Ga . Bb = (Ga . B') + ((Path_product A) . b) by A4, A8, A17, A25, A27, A26;
hence Gs . Bb = (Ga . Bb) * (Det B) by A28, VECTSP_1:def 18; :: thesis: verum

end;

end;

end;

Gs . {} = 0. K by A11, FVSUM_1:8;
then A29: S₁[ {}. (Permutations n)] by A9, VECTSP_1:39;
for B being Element of Fin (Permutations n) holds S₁[B] from SETWISEO:sch 2(A29, A14);
hence Det (A * B) = (Det A) * (Det B) by A10, A5; :: thesis: verum