let n be Nat; :: thesis: for K being Field
for nt, nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K
for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
let K be Field; :: thesis: for nt, nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K
for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
let nt, nt1, nt2 be Element of n -tuples_on NAT; :: thesis: for M being Matrix of K
for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
let M be Matrix of K; :: thesis: for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
let perm be Element of Permutations n; :: thesis: ( nt1 = nt2 * perm implies ( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) ) )
assume A1: nt1 = nt2 * perm ; :: thesis: ( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
reconsider Perm = perm as Permutation of (Seg n) by MATRIX_1:def 12;
Segm (M,nt1,nt) = (Segm (M,nt2,nt)) * Perm by A1, Th33;
hence Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) by MATRIX11:46; :: thesis: Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm)
thus Det (Segm (M,nt,nt1)) = Det ((Segm (M,nt,nt1)) @) by MATRIXR2:43
.= Det (((Segm (M,nt,nt2)) @) * Perm) by A1, Th34
.= - ((Det ((Segm (M,nt,nt2)) @)),perm) by MATRIX11:46
.= - ((Det (Segm (M,nt,nt2))),perm) by MATRIXR2:43 ; :: thesis: verum