let n be Nat; :: thesis: for K being commutative Ring st not K is degenerated & K is domRing-like & K is well-unital holds
for M being Matrix of n + 2,n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
let K be commutative Ring; :: thesis: ( not K is degenerated & K is domRing-like & K is well-unital implies for M being Matrix of n + 2,n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M) )
assume A0: ( not K is degenerated & K is domRing-like & K is well-unital ) ; :: thesis: for M being Matrix of n + 2,n + 2,K
for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
set n2 = n + 2;
let M be Matrix of n + 2,n + 2,K; :: thesis: for perm2 being Element of Permutations (n + 2)
for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
let perm2 be Element of Permutations (n + 2); :: thesis: for Perm2 being Permutation of (Seg (n + 2)) st perm2 = Perm2 holds
Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
let Perm2 be Permutation of (Seg (n + 2)); :: thesis: ( perm2 = Perm2 implies Det (M * Perm2) = (sgn (perm2,K)) * (Det M) )
assume A1: perm2 = Perm2 ; :: thesis: Det (M * Perm2) = (sgn (perm2,K)) * (Det M)
set PathM = Path_product M;
set Mperm = M * Perm2;
set P = Permutations (n + 2);
set KK = the carrier of K;
set aa = the addF of K;
set PathMp = Path_product (M * Perm2);
set F = In ((Permutations (n + 2)),(Fin (Permutations (n + 2))));
reconsider perm29 = perm2 " as Element of Permutations (n + 2) by MATRIX_7:18;
Permutations (n + 2) in Fin (Permutations (n + 2)) by FINSUB_1:def 5;
then A2: In ((Permutations (n + 2)),(Fin (Permutations (n + 2)))) = Permutations (n + 2) by SUBSET_1:def 8;
then consider GM being Function of (Fin (Permutations (n + 2))), the carrier of K such that
A3: Det M = GM . (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) and
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GM . {} = e and
A4: for x being Element of Permutations (n + 2) holds GM . {x} = (Path_product M) . x and
A5: for B9 being Element of Fin (Permutations (n + 2)) st B9 c= In ((Permutations (n + 2)),(Fin (Permutations (n + 2)))) & B9 <> {} holds
for x being Element of Permutations (n + 2) st x in (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) \ B9 holds
GM . (B9 \/ {x}) = the addF of K . ((GM . B9),((Path_product M) . x)) by SETWISEO:def 3;
consider PERM being Permutation of (Permutations (n + 2)) such that
A6: for p being Element of Permutations (n + 2) holds PERM . p = p * perm29 by Th44;
consider GMp being Function of (Fin (Permutations (n + 2))), the carrier of K such that
A7: Det (M * Perm2) = GMp . (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) and
for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GMp . {} = e and
A8: for x being Element of Permutations (n + 2) holds GMp . {x} = (Path_product (M * Perm2)) . x and
A9: for B9 being Element of Fin (Permutations (n + 2)) st B9 c= In ((Permutations (n + 2)),(Fin (Permutations (n + 2)))) & B9 <> {} holds
for x being Element of Permutations (n + 2) st x in (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) \ B9 holds
GMp . (B9 \/ {x}) = the addF of K . ((GMp . B9),((Path_product (M * Perm2)) . x)) by A2, SETWISEO:def 3;
defpred S1[ Nat] means ( $1 <> 0 implies for B being Element of Fin (Permutations (n + 2)) st card B = $1 holds
(sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B) );
A10: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
assume k + 1 <> 0 ; :: thesis: for B being Element of Fin (Permutations (n + 2)) st card B = k + 1 holds
(sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B)
let B be Element of Fin (Permutations (n + 2)); :: thesis: ( card B = k + 1 implies (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B) )
assume A12: card B = k + 1 ; :: thesis: (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B)
per cases ( k = 0 or k > 0 ) ;
suppose k = 0 ; :: thesis: (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B)
then consider x being object such that
A13: B = {x} by A12, CARD_2:42;
A14: x in B by A13, TARSKI:def 1;
B c= Permutations (n + 2) by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations (n + 2) by A14;
A15: GM . {(PERM . x)} = (Path_product M) . (PERM . x) by A4;
A16: PERM . x = x * perm29 by A6;
A17: Permutations (n + 2) = dom PERM by FUNCT_2:52;
GMp . {x} = (Path_product (M * Perm2)) . x by A8;
then (sgn (perm2,K)) * (GMp . B) = GM . {(PERM . x)} by A0, A1, A13, A15, A16, Th43;
then (sgn (perm2,K)) * (GMp . B) = GM . (Im (PERM,x)) by A17, FUNCT_1:59;
hence (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B) by A13; :: thesis: verum
end;
suppose A18: k > 0 ; :: thesis: (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B)
consider x being object such that
A19: x in B by A12, CARD_1:27, XBOOLE_0:def 1;
B c= Permutations (n + 2) by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations (n + 2) by A19;
PERM .: (B \ {x}) c= rng PERM by RELAT_1:111;
then A20: PERM .: (B \ {x}) c= Permutations (n + 2) by FUNCT_2:def 3;
reconsider Px = PERM . x as Element of Permutations (n + 2) ;
A21: Px in {Px} by TARSKI:def 1;
dom PERM = Permutations (n + 2) by FUNCT_2:52;
then A22: Im (PERM,x) = {Px} by FUNCT_1:59;
A23: B c= Permutations (n + 2) by FINSUB_1:def 5;
then B \ {x} c= Permutations (n + 2) ;
then reconsider B9 = B \ {x}, PeBx = PERM .: (B \ {x}), PeB = PERM .: B as Element of Fin (Permutations (n + 2)) by A20, FINSUB_1:def 5;
A24: {x} \/ B9 = B by A19, ZFMISC_1:116;
then A25: PERM .: B = (Im (PERM,x)) \/ PeBx by RELAT_1:120;
PERM . x = x * perm29 by A6;
then A26: (sgn (perm2,K)) * ((Path_product (M * Perm2)) . x) = (Path_product M) . Px by A1, Th43, A0;
A27: dom PERM = Permutations (n + 2) by FUNCT_2:52;
B9 misses {x} by XBOOLE_1:79;
then B9 /\ {x} = {} ;
then PERM .: {} = {Px} /\ PeBx by A22, FUNCT_1:62;
then not Px in PeBx by A21, XBOOLE_0:def 4;
then A28: Px in (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) \ PeBx by A2, XBOOLE_0:def 5;
A29: B9 c= Permutations (n + 2) by FINSUB_1:def 5;
A30: not x in B9 by ZFMISC_1:56;
then A31: x in (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) \ B9 by A2, XBOOLE_0:def 5;
A32: k + 1 = (card B9) + 1 by A12, A24, A30, CARD_2:41;
then ex y being object st y in B9 by A18, CARD_1:27, XBOOLE_0:def 1;
then GM . PeB = the addF of K . ((GM . PeBx),((Path_product M) . Px)) by A2, A5, A20, A25, A22, A28, A29, A27;
then GM . PeB = ((sgn (perm2,K)) * (GMp . B9)) + ((sgn (perm2,K)) * ((Path_product (M * Perm2)) . x)) by A11, A18, A32, A26
.= (sgn (perm2,K)) * ((GMp . B9) + ((Path_product (M * Perm2)) . x)) by VECTSP_1:def 7
.= (sgn (perm2,K)) * (GMp . B) by A2, A9, A18, A23, A24, A32, A31, CARD_1:27, XBOOLE_1:1 ;
hence (sgn (perm2,K)) * (GMp . B) = GM . (PERM .: B) ; :: thesis: verum
end;
end;
end;
A33: S1[ 0 ] ;
A34: for k being Nat holds S1[k] from NAT_1:sch 2(A33, A10);
 A35: rng PERM = Permutations (n + 2) by FUNCT_2:def 3;
A36: dom PERM = Permutations (n + 2) by FUNCT_2:52;
A37: PERM .: (dom PERM) = rng PERM by RELAT_1:113;
A38: (1_ K) * (1_ K) = (- (1_ K)) * (- (1_ K)) by VECTSP_1:10;
A39: ( sgn (perm2,K) = 1_ K or sgn (perm2,K) = - (1_ K) ) by Th11;
card (In ((Permutations (n + 2)),(Fin (Permutations (n + 2))))) <> 0 by A2;
then (sgn (perm2,K)) * (Det (M * Perm2)) = Det M by A2, A3, A7, A34, A37, A36, A35;
hence (sgn (perm2,K)) * (Det M) = (1_ K) * (Det (M * Perm2)) by A39, A38, GROUP_1:def 3
.= Det (M * Perm2) ;
:: thesis: verum