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: [:(Seg n),(Seg n):] c= Indices M by MATRIX_0:24;
A2: len M = n by MATRIX_0:24;
then A3: the_rank_of M <= n by Th74;
A4: width M = n by MATRIX_0:24;
then A5: M = Segm (M,(Seg n),(Seg n)) by A2, Th46
.= EqSegm (M,(Seg n),(Seg n)) by Def3 ;
A6: card (Seg n) = n by FINSEQ_1:57;
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
A7: [:P,Q:] c= Indices M and
A8: card P = card Q and
A9: card P = n and
A10: Det (EqSegm (M,P,Q)) <> 0. K by Def4;
P c= Seg n by A2, A7, A8, Th67;
then A11: P = Seg n by A6, A9, CARD_2:102;
Q c= Seg n by A4, A7, A8, Th67;
then Q = Seg n by A6, A8, A9, CARD_2:102;
then M = Segm (M,P,Q) by A2, A4, A11, Th46
.= EqSegm (M,P,Q) by A8, Def3 ;
hence Det M <> 0. K by A9, A10; :: thesis: verum

end;

assume Det M <> 0. K ; :: thesis: the_rank_of M = n
then the_rank_of M >= n by A6, A5, A1, Def4;
hence the_rank_of M = n by A3, XXREAL_0:1; :: thesis: verum