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 ) ) )
A1: len M = m by MATRIX_1:def 3;
A2: card (Seg n) = n by FINSEQ_1:78;
A3: 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 that
A4: W is linearly-independent and
A5: W c= lines M ; :: thesis: card W <= the_rank_of M
consider P1 being finite without_zero Subset of NAT such that
A6: P1 c= Seg m and
A7: lines (Segm M,P1,(Seg n)) = W and
A8: Segm M,P1,(Seg n) is without_repeated_line by A5, Th122;
set S1 = Segm M,P1,(Seg n);
A9: (Segm M,P1,(Seg n)) .: (dom (Segm M,P1,(Seg n))) = lines (Segm M,P1,(Seg n)) by RELAT_1:146;
dom (Segm M,P1,(Seg n)),(Segm M,P1,(Seg n)) .: (dom (Segm M,P1,(Seg n))) are_equipotent by A8, CARD_1:60;
then A10: card W = card (dom (Segm M,P1,(Seg n))) by A7, A9, 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 A10; :: thesis: verum

end;

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

then Seg m <> {} by A6;
then X: m <> 0 ;
then A12: len M = m by Th1;
width M = n by Th1, X;
then [:P1,(Seg n):] c= [:(Seg (len M)),(Seg (width M)):] by A6, A12, 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 A2, A4, A7, A8, A10, Th121; :: thesis: verum

end;

end;

end;

A13: 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;

consider P, Q being finite without_zero Subset of NAT such that
A14: [:P,Q:] c= Indices M and
A15: card P = card Q and
A16: card P = the_rank_of M and
A17: Det (EqSegm M,P,Q) <> 0. K by Def4;
Q c= Seg (width M) by A14, A15, Th67;
then A18: Q c= Seg n by A13, XBOOLE_1:1;
set S = Segm M,P,(Seg n);
A19: len (Segm M,P,(Seg n)) = card P by MATRIX_1:def 3;
Segm M,P,Q = EqSegm M,P,Q by A15, Def3;
then A20: the_rank_of (EqSegm M,P,Q) <= the_rank_of (Segm M,P,(Seg n)) by A18, Th80;
A21: the_rank_of (Segm M,P,(Seg n)) <= len (Segm M,P,(Seg n)) by Th74;
the_rank_of (EqSegm M,P,Q) = card P by A17, Th83;
then A22: the_rank_of (Segm M,P,(Seg n)) = card P by A20, A19, A21, XXREAL_0:1;
then A23: lines (Segm M,P,(Seg n)) is linearly-independent by Th121;
Segm M,P,(Seg n) is without_repeated_line by A22, Th121;
then A24: dom (Segm M,P,(Seg n)),(Segm M,P,(Seg n)) .: (dom (Segm M,P,(Seg n))) are_equipotent by CARD_1:60;
(Segm M,P,(Seg n)) .: (dom (Segm M,P,(Seg n))) = lines (Segm M,P,(Seg n)) by RELAT_1:146;
then A25: card (lines (Segm M,P,(Seg n))) = card (dom (Segm M,P,(Seg n))) by A24, 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 ;
A26: P c= Seg (len M) by A14, A15, Th67;
then lines (Segm M,P,(Seg n)) c= lines M by A1, Th118;
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 A16, A23, A25, A2, A3; :: 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
A27: ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = R ) and
A28: 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
A29: R <= the_rank_of M by A3, A27;
the_rank_of M <= R by A16, A23, A25, A26, A1, A2, A28, Th118;
hence the_rank_of M = R by A29, XXREAL_0:1; :: thesis: verum