let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds
( the_rank_of M = n iff Det M <> 0. K )
let K be Field; :: thesis: for M being Matrix of n,K holds
( the_rank_of M = n iff Det M <> 0. K )
let M be Matrix of n,K; :: thesis: ( the_rank_of M = n iff Det M <> 0. K )
A1: ( len M = n & width M = n & card (Seg n) = n ) by FINSEQ_1:78, MATRIX_1:25;
thus ( the_rank_of M = n implies Det M <> 0. K ) :: thesis: ( Det M <> 0. K implies the_rank_of M = n )

proof

assume the_rank_of M = n ; :: thesis: Det M <> 0. K
then consider P, Q being finite without_zero Subset of NAT such that
A2: ( [:P,Q:] c= Indices M & card P = card Q & card P = n ) and
A3: Det (EqSegm M,P,Q) <> 0. K by Def4;
( P c= Seg n & Q c= Seg n ) by A1, A2, Th67;
then ( P = Seg n & Q = Seg n ) by A1, A2, CARD_FIN:1;
then M = Segm M,P,Q by A1, Th46
.= EqSegm M,P,Q by A2, Def3 ;
hence Det M <> 0. K by A2, A3; :: thesis: verum

end;

assume A4: Det M <> 0. K ; :: thesis: the_rank_of M = n
M = Segm M,(Seg n),(Seg n) by A1, Th46
.= EqSegm M,(Seg n),(Seg n) by Def3 ;
then ( [:(Seg n),(Seg n):] c= Indices M & Det M = Det (EqSegm M,(Seg n),(Seg n)) ) by FINSEQ_1:78, MATRIX_1:25;
then ( the_rank_of M >= n & the_rank_of M <= n ) by A1, A4, Def4, Th74;
hence the_rank_of M = n by XXREAL_0:1; :: thesis: verum