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_0:def 2;
A2: card (Seg n) = n by FINSEQ_1:57;
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:113;
dom (Segm (M,P1,(Seg n))),(Segm (M,P1,(Seg n))) .: (dom (Segm (M,P1,(Seg n)))) are_equipotent by A8, CARD_1:33;
then A10: card W = card (dom (Segm (M,P1,(Seg n)))) by A7, A9, CARD_1:5
.= card (Seg (len (Segm (M,P1,(Seg n))))) by FINSEQ_1:def 3
.= card (Seg (card P1)) by MATRIX_0:def 2
.= card P1 by FINSEQ_1:57 ;

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 A11: m <> 0 ;
then A12: len M = m by Th1;
width M = n by Th1, A11;
then [:P1,(Seg n):] c= [:(Seg (len M)),(Seg (width M)):] by A6, A12, ZFMISC_1:96;
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 :: thesis: Seg (width M) c= Seg n

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_0:def 3;
hence Seg (width M) c= Seg n ; :: thesis: verum

end;

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

then m > 0 by MATRIX_0:def 2;
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;
set S = Segm (M,P,(Seg n));
A19: len (Segm (M,P,(Seg n))) = card P by MATRIX_0:def 2;
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:33;
(Segm (M,P,(Seg n))) .: (dom (Segm (M,P,(Seg n)))) = lines (Segm (M,P,(Seg n))) by RELAT_1:113;
then A25: card (lines (Segm (M,P,(Seg n)))) = card (dom (Segm (M,P,(Seg n)))) by A24, CARD_1:5
.= card (Seg (len (Segm (M,P,(Seg n))))) by FINSEQ_1:def 3
.= card (Seg (card P)) by MATRIX_0:def 2
.= card P by FINSEQ_1:57 ;
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