let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line
let K be Field; :: thesis: for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line
let M be Matrix of m,n,K; :: thesis: ( the_rank_of M = m implies M is without_repeated_line )
assume A1: the_rank_of M = m ; :: thesis: M is without_repeated_line
A2: len M = m by MATRIX_0:def 2;
assume not M is without_repeated_line ; :: thesis: contradiction
then consider x1, x2 being object such that
A3: x1 in dom M and
A4: x2 in dom M and
A5: M . x1 = M . x2 and
A6: x1 <> x2 ;
reconsider x1 = x1, x2 = x2 as Element of NAT by A3, A4;
consider k being Nat such that
A7: len M = k + 1 and
A8: len (Del (M,x1)) = k by A3, FINSEQ_3:104;
A9: dom M = Seg (len M) by FINSEQ_1:def 3;
then A10: M . x2 = Line (M,x2) by A4, A2, MATRIX_0:52;
M . x1 = Line (M,x1) by A3, A9, A2, MATRIX_0:52;
then M = RLine (M,x1,(Line (M,x2))) by A5, A10, MATRIX11:30
.= RLine (M,x1,((1_ K) * (Line (M,x2)))) by FVSUM_1:57 ;
then m = the_rank_of (DelLine (M,x1)) by A1, A4, A6, A9, Th93;
then m <= k by A8, Th74;
hence contradiction by A2, A7, NAT_1:13; :: thesis: verum