let K be Field; for M being Matrix of K holds
( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) )
let M be Matrix of K; ( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) )
set r = the_rank_of M;
thus
( the_rank_of M > 0 implies ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) )
( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) implies the_rank_of M > 0 )proof
consider P,
Q being
finite without_zero Subset of
NAT such that A1:
[:P,Q:] c= Indices M
and A2:
card P = card Q
and A3:
card P = the_rank_of M
and A4:
Det (EqSegm (M,P,Q)) <> 0. K
by Def4;
assume
the_rank_of M > 0
;
ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K )
then consider x being
object such that A5:
x in P
by A3, CARD_1:27, XBOOLE_0:def 1;
reconsider x =
x as non
zero Element of
NAT by A5;
{x} c= P
by A5, ZFMISC_1:31;
then consider Q1 being
finite without_zero Subset of
NAT such that A6:
Q1 c= Q
and A7:
card {x} = card Q1
and A8:
Det (EqSegm (M,{x},Q1)) <> 0. K
by A2, A4, Th65;
consider y being
object such that A9:
{y} = Q1
by A7, CARD_2:42;
y in {y}
by TARSKI:def 1;
then reconsider y =
y as non
zero Element of
NAT by A9;
take
x
;
ex j being Nat st
( [x,j] in Indices M & M * (x,j) <> 0. K )
take
y
;
( [x,y] in Indices M & M * (x,y) <> 0. K )
y in Q1
by A9, TARSKI:def 1;
then
[x,y] in [:P,Q:]
by A5, A6, ZFMISC_1:87;
hence
[x,y] in Indices M
by A1;
M * (x,y) <> 0. K
A10:
card {x} = 1
by CARD_1:30;
EqSegm (
M,
{x},
Q1) =
Segm (
M,
{x},
{y})
by A7, A9, Def3
.=
<*<*(M * (x,y))*>*>
by Th44
;
hence
M * (
x,
y)
<> 0. K
by A8, A10, MATRIX_3:34;
verum
end;
given i, j being Nat such that A11:
[i,j] in Indices M
and
A12:
M * (i,j) <> 0. K
; the_rank_of M > 0
A13:
j in Seg (width M)
by A11, ZFMISC_1:87;
Indices M = [:(Seg (len M)),(Seg (width M)):]
by FINSEQ_1:def 3;
then A14:
i in Seg (len M)
by A11, ZFMISC_1:87;
then reconsider i = i, j = j as non zero Element of NAT by A13;
A15:
card {i} = 1
by CARD_1:30;
A16:
card {j} = 1
by CARD_1:30;
then EqSegm (M,{i},{j}) =
Segm (M,{i},{j})
by Def3, CARD_1:30
.=
<*<*(M * (i,j))*>*>
by Th44
;
then A17:
Det (EqSegm (M,{i},{j})) <> 0. K
by A12, A15, MATRIX_3:34;
A18:
{j} c= Seg (width M)
by A13, ZFMISC_1:31;
{i} c= Seg (len M)
by A14, ZFMISC_1:31;
then
[:{i},{j}:] c= Indices M
by A15, A16, A18, Th67;
hence
the_rank_of M > 0
by A15, A16, A17, Def4; verum