let m, n be Nat; 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; 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; ( the_rank_of M = m implies M is without_repeated_line )
assume A1:
the_rank_of M = m
; M is without_repeated_line
A2:
len M = m
by MATRIX_0:def 2;
assume
not M is without_repeated_line
; 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; verum