let n be Nat; :: thesis: for K being Field
for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))
let K be Field; :: thesis: for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))
let M be Matrix of K; :: thesis: for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))
let nt, nt1, nt9, nt19 be Element of n -tuples_on NAT; :: thesis: ( rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) implies Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
assume that
A1: rng nt = rng nt9 and
A2: rng nt1 = rng nt19 ; :: thesis: ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
set S19 = Segm (M,nt,nt19);
set S9 = Segm (M,nt9,nt19);
set S = Segm (M,nt,nt1);
per cases ( not nt is one-to-one or not nt1 is one-to-one or ( nt is one-to-one & nt1 is one-to-one ) ) ;
suppose A3: ( not nt is one-to-one or not nt1 is one-to-one ) ; :: thesis: ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
then A4: Det (Segm (M,nt,nt1)) = 0. K by Th27, Th31;
( not nt9 is one-to-one or not nt19 is one-to-one ) by A1, A2, A3, Lm1;
hence ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) ) by A4, Th27, Th31; :: thesis: verum
end;
suppose A5: ( nt is one-to-one & nt1 is one-to-one ) ; :: thesis: ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
then nt19 is one-to-one by A2, Lm1;
then consider perm1 being Permutation of (Seg n) such that
A6: nt1 = nt19 * perm1 by A2, A5, Th32;
nt9 is one-to-one by A1, A5, Lm1;
then consider perm being Permutation of (Seg n) such that
A7: nt = nt9 * perm by A1, A5, Th32;
reconsider perm = perm, perm1 = perm1 as Element of Permutations n by MATRIX_1:def 12;
per cases ( perm1 is even or perm1 is odd ) ;
suppose A8: perm1 is even ; :: thesis: ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt19))),perm1) by A6, Th35;
then A9: Det (Segm (M,nt,nt1)) = Det (Segm (M,nt,nt19)) by A8, MATRIX_1:def 16;
Det (Segm (M,nt,nt19)) = - ((Det (Segm (M,nt9,nt19))),perm) by A7, Th35;
hence ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) ) by A9, MATRIX_1:def 16; :: thesis: verum
end;
suppose A10: perm1 is odd ; :: thesis: ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) )
Det (Segm (M,nt,nt19)) = - ((Det (Segm (M,nt9,nt19))),perm) by A7, Th35;
then A11: ( Det (Segm (M,nt,nt19)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt19)) = - (Det (Segm (M,nt9,nt19))) ) by MATRIX_1:def 16;
Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt19))),perm1) by A6, Th35;
then Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt,nt19))) by A10, MATRIX_1:def 16;
then ( Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) or Det (Segm (M,nt,nt1)) = (0. K) + (- (- (Det (Segm (M,nt9,nt19))))) ) by A11, RLVECT_1:def 4;
then ( Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) or Det (Segm (M,nt,nt1)) = (0. K) - (- (Det (Segm (M,nt9,nt19)))) ) ;
then ( Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) or (Det (Segm (M,nt,nt1))) + (- (Det (Segm (M,nt9,nt19)))) = 0. K ) by VECTSP_2:2;
hence ( Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) or Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19))) ) by VECTSP_1:19; :: thesis: verum
end;
end;
end;
end;