let i, j, m be Nat; :: thesis: for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds
Det (Segm (M,mt1,mt)) = 0. K
let K be Field; :: thesis: for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds
Det (Segm (M,mt1,mt)) = 0. K
let mt, mt1 be Element of m -tuples_on NAT; :: thesis: for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds
Det (Segm (M,mt1,mt)) = 0. K
let M be Matrix of K; :: thesis: ( i in Seg m & j in Seg m & mt . i = mt . j & i <> j implies Det (Segm (M,mt1,mt)) = 0. K )
assume that
A1: i in Seg m and
A2: j in Seg m and
A3: mt . i = mt . j and
A4: i <> j ; :: thesis: Det (Segm (M,mt1,mt)) = 0. K
A5: ( i < j or j < i ) by A4, XXREAL_0:1;
set S = Segm (M,mt1,mt);
A6: width (Segm (M,mt1,mt)) = m by MATRIX_0:24;
then A7: Col ((Segm (M,mt1,mt)),j) = Line (((Segm (M,mt1,mt)) @),j) by A2, MATRIX_0:59;
Col ((Segm (M,mt1,mt)),i) = Line (((Segm (M,mt1,mt)) @),i) by A1, A6, MATRIX_0:59;
hence 0. K = Det ((Segm (M,mt1,mt)) @) by A1, A2, A3, A7, A5, Th29, MATRIX11:50
.= Det (Segm (M,mt1,mt)) by MATRIXR2:43 ;
:: thesis: verum