let n be Nat; 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; 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; 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; 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; ( 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
; ( 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; 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
; verum