let n be Nat; :: thesis: for K being Field
for nt1, nt2, nt 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 nt1, nt2, nt 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 nt1, nt2, nt 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_2:def 11;
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