let i, m, j 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_1:25;
then A7: Col (Segm M,mt1,mt),j = Line ((Segm M,mt1,mt) @ ),j by A2, MATRIX_2:17;
Col (Segm M,mt1,mt),i = Line ((Segm M,mt1,mt) @ ),i by A1, A6, MATRIX_2:17;
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