let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= RANK ) ) )
let K be Field; :: thesis: for M being Matrix of m,n,K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= RANK ) ) )
let M be Matrix of m,n,K; :: thesis: for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= RANK ) ) )
let R be Element of NAT ; :: thesis: ( the_rank_of M = R iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = R ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= R ) ) )
consider P, Q being finite without_zero Subset of NAT such that
A1: ( [:P,Q:] c= Indices M & card P = card Q ) and
A2: ( card P = the_rank_of M & Det (EqSegm M,P,Q) <> 0. K ) by Def4;

A3: now

per cases ( len M = 0 or len M > 0 ) ;

suppose len M = 0 ; :: thesis: Seg (width M) c= Seg n

then width M = 0 by MATRIX_1:def 4;
hence Seg (width M) c= Seg n by FINSEQ_1:7; :: thesis: verum

end;

suppose len M > 0 ; :: thesis: Seg (width M) c= Seg n

then m > 0 by MATRIX_1:def 3;
hence Seg (width M) c= Seg n by Th1; :: thesis: verum

end;

end;

end;

set S = Segm M,P,(Seg n);
Q c= Seg (width M) by A1, Th67;
then ( Q c= Seg n & Segm M,P,Q = EqSegm M,P,Q ) by A1, A3, Def3, XBOOLE_1:1;
then ( the_rank_of (EqSegm M,P,Q) <= the_rank_of (Segm M,P,(Seg n)) & the_rank_of (EqSegm M,P,Q) = card P & len (Segm M,P,(Seg n)) = card P & the_rank_of (Segm M,P,(Seg n)) <= len (Segm M,P,(Seg n)) ) by A2, Th74, Th80, Th83, MATRIX_1:def 3;
then the_rank_of (Segm M,P,(Seg n)) = card P by XXREAL_0:1;
then A4: ( lines (Segm M,P,(Seg n)) is linearly-independent & Segm M,P,(Seg n) is without_repeated_line ) by Th121;
then ( dom (Segm M,P,(Seg n)),(Segm M,P,(Seg n)) .: (dom (Segm M,P,(Seg n))) are_equipotent & (Segm M,P,(Seg n)) .: (dom (Segm M,P,(Seg n))) = lines (Segm M,P,(Seg n)) ) by CARD_1:60, RELAT_1:146;
then A5: card (lines (Segm M,P,(Seg n))) = card (dom (Segm M,P,(Seg n))) by CARD_1:21
.= card (Seg (len (Segm M,P,(Seg n)))) by FINSEQ_1:def 3
.= card (Seg (card P)) by MATRIX_1:def 3
.= card P by FINSEQ_1:78 ;
( P c= Seg (len M) & len M = m ) by A1, Th67, MATRIX_1:def 3;
then A6: lines (Segm M,P,(Seg n)) c= lines M by Th118;
A7: card (Seg n) = n by FINSEQ_1:78;
A8: for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= the_rank_of M

proof

let W be finite Subset of (n -VectSp_over K); :: thesis: ( W is linearly-independent & W c= lines M implies card W <= the_rank_of M )
assume A9: ( W is linearly-independent & W c= lines M ) ; :: thesis: card W <= the_rank_of M
consider P1 being finite without_zero Subset of NAT such that
A10: ( P1 c= Seg m & lines (Segm M,P1,(Seg n)) = W ) and
A11: Segm M,P1,(Seg n) is without_repeated_line by A9, Th122;
set S1 = Segm M,P1,(Seg n);
( dom (Segm M,P1,(Seg n)),(Segm M,P1,(Seg n)) .: (dom (Segm M,P1,(Seg n))) are_equipotent & (Segm M,P1,(Seg n)) .: (dom (Segm M,P1,(Seg n))) = lines (Segm M,P1,(Seg n)) ) by A11, CARD_1:60, RELAT_1:146;
then A12: card W = card (dom (Segm M,P1,(Seg n))) by A10, CARD_1:21
.= card (Seg (len (Segm M,P1,(Seg n)))) by FINSEQ_1:def 3
.= card (Seg (card P1)) by MATRIX_1:def 3
.= card P1 by FINSEQ_1:78 ;

per cases ( card P1 = 0 or card P1 > 0 ) ;

suppose card P1 = 0 ; :: thesis: card W <= the_rank_of M

hence card W <= the_rank_of M by A12; :: thesis: verum

end;

suppose card P1 > 0 ; :: thesis: card W <= the_rank_of M

then Seg m <> {} by A10;
then ( width M = n & len M = m ) by Th1, FINSEQ_1:4;
then [:P1,(Seg n):] c= [:(Seg (len M)),(Seg (width M)):] by A10, ZFMISC_1:119;
then [:P1,(Seg n):] c= Indices M by FINSEQ_1:def 3;
then the_rank_of (Segm M,P1,(Seg n)) <= the_rank_of M by Th79;
hence card W <= the_rank_of M by A7, A9, A10, A11, A12, Th121; :: thesis: verum

end;

end;

end;

hence ( the_rank_of M = R implies ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = R ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= R ) ) ) by A2, A4, A5, A6, A7; :: thesis: ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = R ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= R ) implies the_rank_of M = R )
assume that
A13: ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = R ) and
A14: for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= R ; :: thesis: the_rank_of M = R
( the_rank_of M <= R & R <= the_rank_of M ) by A2, A4, A5, A6, A7, A8, A13, A14;
hence the_rank_of M = R by XXREAL_0:1; :: thesis: verum