let n be Nat; :: thesis: for K being commutative Ring
for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
let K be commutative Ring; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i < j holds
for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i < j implies for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i < j ; :: thesis: for M being Matrix of n,K st Line (M,i) = Line (M,j) holds
Det M = 0. K
set P = Permutations n;
consider Q, E being finite set such that
( E = { p where p is Element of Permutations n : p is even } & Q = { q where q is Element of Permutations n : q is odd } ) and
A4: ( E /\ Q = {} & E \/ Q = Permutations n ) and
A5: ex P being Function of E,Q ex tr being Element of Permutations n st
( tr is being_transposition & tr . i = j & dom P = E & P is bijective & ( for p being Element of Permutations n st p in E holds
P . p = p * tr ) ) by A1, A2, A3, Lm8;
A6: E c= Permutations n by A4, XBOOLE_1:7;
set KK = the carrier of K;
set aa = the addF of K;
let M be Matrix of n,K; :: thesis: ( Line (M,i) = Line (M,j) implies Det M = 0. K )
assume A7: Line (M,i) = Line (M,j) ; :: thesis: Det M = 0. K
A8: Q c= Permutations n by A4, XBOOLE_1:7;
set PathM = Path_product M;
consider PERM being Function of E,Q, tr being Element of Permutations n such that
A9: tr is being_transposition and
A10: tr . i = j and
A11: dom PERM = E and
A12: PERM is bijective and
A13: for p being Element of Permutations n st p in E holds
PERM . p = p * tr by A5;
reconsider E = E, Q = Q as Element of Fin (Permutations n) by A6, A8, FINSUB_1:def 5;
the addF of K is having_a_unity by FVSUM_1:8;
then consider GE being Function of (Fin (Permutations n)), the carrier of K such that
A14: the addF of K $$ (E,(Path_product M)) = GE . E and
A15: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GE . {} = e and
A16: for x being Element of Permutations n holds GE . {x} = (Path_product M) . x and
A17: for B9 being Element of Fin (Permutations n) st B9 c= E & B9 <> {} holds
for x being Element of Permutations n st x in E \ B9 holds
GE . (B9 \/ {x}) = the addF of K . ((GE . B9),((Path_product M) . x)) by SETWISEO:def 3;
A18: E misses Q by A4;
the addF of K is having_a_unity by FVSUM_1:8;
then consider GQ being Function of (Fin (Permutations n)), the carrier of K such that
A19: the addF of K $$ (Q,(Path_product M)) = GQ . Q and
A20: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
GQ . {} = e and
A21: for x being Element of Permutations n holds GQ . {x} = (Path_product M) . x and
A22: for B9 being Element of Fin (Permutations n) st B9 c= Q & B9 <> {} holds
for x being Element of Permutations n st x in Q \ B9 holds
GQ . (B9 \/ {x}) = the addF of K . ((GQ . B9),((Path_product M) . x)) by SETWISEO:def 3;
defpred S1[ Nat] means for B, PB being Element of Fin (Permutations n) st card B = $1 & B c= E & PERM .: B = PB holds
(GE . B) + (GQ . PB) = 0. K;
A23: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A24: S1[k] ; :: thesis: S1[k + 1]
let B, PB be Element of Fin (Permutations n); :: thesis: ( card B = k + 1 & B c= E & PERM .: B = PB implies (GE . B) + (GQ . PB) = 0. K )
assume that
A25: card B = k + 1 and
A26: B c= E and
A27: PERM .: B = PB ; :: thesis: (GE . B) + (GQ . PB) = 0. K
now :: thesis: ( ( k = 0 & (GE . B) + (GQ . PB) = 0. K ) or ( k > 0 & (GQ . PB) + (GE . B) = 0. K ) )
per cases ( k = 0 or k > 0 ) ;
case k = 0 ; :: thesis: (GE . B) + (GQ . PB) = 0. K
then consider x being object such that
A28: B = {x} by A25, CARD_2:42;
A29: x in B by A28, TARSKI:def 1;
B c= Permutations n by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations n by A29;
x * tr is Element of Permutations n by MATRIX_9:39;
then reconsider Px = PERM . x as Element of Permutations n by A13, A26, A29;
A30: Im (PERM,x) = {Px} by A11, A26, A29, FUNCT_1:59;
A31: GE . {x} = (Path_product M) . x by A16;
A32: GQ . {(PERM . x)} = (Path_product M) . Px by A21;
Px = x * tr by A13, A26, A29;
then - (GE . B) = GQ . PB by A1, A2, A3, A7, A9, A10, A27, A28, A31, A32, A30, Th49;
hence (GE . B) + (GQ . PB) = 0. K by RLVECT_1:def 10; :: thesis: verum
end;
case A33: k > 0 ; :: thesis: (GQ . PB) + (GE . B) = 0. K
consider x being object such that
A34: x in B by A25, CARD_1:27, XBOOLE_0:def 1;
B c= Permutations n by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations n by A34;
x * tr is Element of Permutations n by MATRIX_9:39;
then reconsider Px = PERM . x as Element of Permutations n by A13, A26, A34;
A35: Im (PERM,x) = {Px} by A11, A26, A34, FUNCT_1:59;
Px = x * tr by A13, A26, A34;
then A36: - ((Path_product M) . x) = (Path_product M) . Px by A1, A2, A3, A7, A9, A10, Th49;
A37: Q c= Permutations n by FINSUB_1:def 5;
B c= Permutations n by FINSUB_1:def 5;
then A38: B \ {x} c= Permutations n ;
A39: rng PERM = Q by A12, FUNCT_2:def 3;
then A40: Px in Q by A11, A26, A34, FUNCT_1:def 3;
PERM .: (B \ {x}) c= rng PERM by RELAT_1:111;
then PERM .: (B \ {x}) c= Permutations n by A39, A37;
then reconsider B9 = B \ {x}, PeBx = PERM .: (B \ {x}) as Element of Fin (Permutations n) by A38, FINSUB_1:def 5;
A41: Px in {Px} by TARSKI:def 1;
A42: {x} \/ B9 = B by A34, ZFMISC_1:116;
then A43: PERM .: B = (Im (PERM,x)) \/ PeBx by RELAT_1:120;
B9 misses {x} by XBOOLE_1:79;
then B9 /\ {x} = {} ;
then PERM .: {} = {Px} /\ PeBx by A12, A35, FUNCT_1:62;
then not Px in PeBx by A41, XBOOLE_0:def 4;
then A44: Px in Q \ PeBx by A40, XBOOLE_0:def 5;
A45: not x in B9 by ZFMISC_1:56;
then A46: x in E \ B9 by A26, A34, XBOOLE_0:def 5;
A47: k + 1 = (card B9) + 1 by A25, A42, A45, CARD_2:41;
then consider y being object such that
A48: y in B9 by A33, CARD_1:27, XBOOLE_0:def 1;
B \ {x} c= E by A26;
then PERM . y in PeBx by A11, A48, FUNCT_1:def 6;
then GQ . PB = the addF of K . ((GQ . PeBx),((Path_product M) . Px)) by A22, A27, A39, A43, A35, A44, RELAT_1:111;
hence (GQ . PB) + (GE . B) = ((GQ . PeBx) - ((Path_product M) . x)) + ((GE . B9) + ((Path_product M) . x)) by A17, A26, A33, A42, A47, A46, A36, CARD_1:27, XBOOLE_1:1
.= (GQ . PeBx) + ((- ((Path_product M) . x)) + ((GE . B9) + ((Path_product M) . x))) by RLVECT_1:def 3
.= (GQ . PeBx) + ((GE . B9) + (((Path_product M) . x) - ((Path_product M) . x))) by RLVECT_1:def 3
.= (GQ . PeBx) + ((GE . B9) + (0. K)) by RLVECT_1:def 10
.= ((GQ . PeBx) + (GE . B9)) + (0. K) by RLVECT_1:def 3
.= (0. K) + (0. K) by A24, A26, A47, XBOOLE_1:1
.= 0. K by RLVECT_1:4 ;
:: thesis: verum
end;
end;
end;
hence (GE . B) + (GQ . PB) = 0. K ; :: thesis: verum
end;
set F = In ((Permutations n),(Fin (Permutations n)));
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A49: Permutations n = In ((Permutations n),(Fin (Permutations n))) by SUBSET_1:def 8;
rng PERM = Q by A12, FUNCT_2:def 3;
then A50: PERM .: E = Q by A11, RELAT_1:113;
A51: S1[ 0 ]
proof
let B, PB be Element of Fin (Permutations n); :: thesis: ( card B = 0 & B c= E & PERM .: B = PB implies (GE . B) + (GQ . PB) = 0. K )
assume that
A52: card B = 0 and
B c= E and
A53: PERM .: B = PB ; :: thesis: (GE . B) + (GQ . PB) = 0. K
A54: B = {} by A52;
then A55: GE . B = 0. K by A15, FVSUM_1:6;
PERM .: {} = {} ;
then GQ . PB = 0. K by A20, A53, A54, FVSUM_1:6;
hence (GE . B) + (GQ . PB) = 0. K by A55, RLVECT_1:def 4; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A51, A23);
 then S1[ card E] ;
then ( the addF of K $$ (E,(Path_product M))) + ( the addF of K $$ (Q,(Path_product M))) = 0. K by A14, A19, A50;
hence Det M = 0. K by A4, A18, A49, FVSUM_1:8, SETWOP_2:4; :: thesis: verum