let n be Nat; :: thesis: for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)
let K be commutative Ring; :: thesis: ( not K is degenerated & K is well-unital & K is domRing-like implies for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B) )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: thesis: for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)
let A, B be Matrix of n,K; :: 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 SUM1 being Function of (Permutations n), the carrier of K such that
A2: Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),SUM1) and
A3: for perm being Element of Permutations n holds SUM1 . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) by A0, A1, Th61;
set Path = Path_product A;
set F = In ((Permutations n),(Fin (Permutations n)));
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A4: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;
then consider Ga being Function of (Fin (Permutations n)), the carrier of K such that
A5: Det A = Ga . (In ((Permutations n),(Fin (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 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
Ga . (B9 \/ {x}) = the addF of K . ((Ga . B9),((Path_product A) . x)) by SETWISEO:def 3;
A9: Ga . {} = 0. K by A6, FVSUM_1:6;
consider Gs being Function of (Fin (Permutations n)), the carrier of K such that
A10: Det (A * B) = Gs . (In ((Permutations n),(Fin (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} = SUM1 . x and
A13: 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
Gs . (B9 \/ {x}) = the addF of K . ((Gs . B9),(SUM1 . x)) by A2, A4, SETWISEO:def 3;
defpred S1[ set ] means for B9 being Element of Fin (Permutations n) st B9 = $1 holds
Gs . B9 = (Ga . B9) * (Det B);
A14: for B9 being Element of Fin (Permutations n)
for b being Element of Permutations n st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin (Permutations n); :: thesis: for b being Element of Permutations n st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of Permutations n; :: thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume that
A15: S1[B9] and
A16: not b in B9 ; :: thesis: S1[B9 \/ {b}]
set mA = the multF of K $$ (Path_matrix (b,A));
let Bb be Element of Fin (Permutations n); :: thesis: ( Bb = B9 \/ {b} implies Gs . Bb = (Ga . Bb) * (Det B) )
assume A17: Bb = B9 \/ {b} ; :: thesis: Gs . Bb = (Ga . Bb) * (Det B)
A18: now :: thesis: SUM1 . b = ((Path_product A) . b) * (Det B)
per cases ( b is even or b is odd ) ;
suppose A19: b is even ; :: thesis: SUM1 . 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_1:def 16;
- ((Det B),b) = Det B by A19, MATRIX_1:def 16;
hence SUM1 . 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: b is odd ; :: thesis: SUM1 . 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_1:def 16;
- ((Det B),b) = - (Det B) by A21, MATRIX_1: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:9
.= - (( the multF of K $$ (Path_matrix (b,A))) * (- ((Det B),b))) by VECTSP_1:9 ;
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:16;
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:19;
- (( the multF of K $$ (Path_matrix (b,A))),b) = (Path_product A) . b by MATRIX_3:def 8;
hence SUM1 . b = ((Path_product A) . b) * (Det B) by A3, A23; :: thesis: verum
end;
end;
end;
per cases ( B9 = {} or B9 <> {} ) ;
suppose A24: B9 = {} ; :: 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: B9 <> {} ; :: thesis: Gs . Bb = (Ga . Bb) * (Det B)
A26: B9 c= Permutations n by FINSUB_1:def 5;
A27: b in (In ((Permutations n),(Fin (Permutations n)))) \ B9 by A4, A16, XBOOLE_0:def 5;
then Gs . Bb = the addF of K . ((Gs . B9),(SUM1 . b)) by A4, A13, A17, A25, A26;
then A28: Gs . Bb = ((Ga . B9) * (Det B)) + (((Path_product A) . b) * (Det B)) by A15, A18;
Ga . Bb = (Ga . B9) + ((Path_product A) . b) by A4, A8, A17, A25, A27, A26;
hence Gs . Bb = (Ga . Bb) * (Det B) by A28, VECTSP_1:def 7; :: thesis: verum
end;
end;
end;
Gs . {} = 0. K by A11, FVSUM_1:6;
then A29: S1[ {}. (Permutations n)] by A9;
for B being Element of Fin (Permutations n) holds S1[B] from SETWISEO:sch 2(A29, A14);
 hence Det (A * B) = (Det A) * (Det B) by A10, A5; :: thesis: verum