let n be Nat; 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; 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; ( 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 )
( Det M <> 0. K implies the_rank_of M = n )proof
assume
the_rank_of M = n
;
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;
verum
end;
assume
Det M <> 0. K
; 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; verum