let K be Field; for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )
let M be Matrix of K; ( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )
thus
( the_rank_of M = 1 implies ( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )
( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) implies the_rank_of M = 1 )proof
assume A1:
the_rank_of M = 1
;
( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) )
hence
ex
i,
j being
Nat st
(
[i,j] in Indices M &
M * (
i,
j)
<> 0. K )
by Th96;
for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n))
let i,
j,
n,
p be
Nat;
( [:{i,j},{n,p}:] c= Indices M implies (M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n)) )
assume A2:
[:{i,j},{n,p}:] c= Indices M
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
per cases
( i = j or n = p or ( i <> j & n <> p ) )
;
suppose
(
i = j or
n = p )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))hence
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
;
verum end; suppose A3:
(
i <> j &
n <> p )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
Indices M = [:(Seg (len M)),(Seg (width M)):]
by FINSEQ_1:def 3;
then A4:
{i,j} c= Seg (len M)
by A2, ZFMISC_1:114;
A5:
i in {i,j}
by TARSKI:def 2;
A6:
n in {n,p}
by TARSKI:def 2;
A7:
p in {n,p}
by TARSKI:def 2;
A8:
j in {i,j}
by TARSKI:def 2;
{n,p} c= Seg (width M)
by A2, ZFMISC_1:114;
then reconsider I =
i,
J =
j,
P =
p,
N =
n as non
zero Element of
NAT by A4, A5, A8, A7, A6;
A9:
card {I,J} = 2
by A3, CARD_2:57;
set JP =
M * (
J,
P);
set JN =
M * (
J,
N);
set IP =
M * (
I,
P);
set IN =
M * (
I,
N);
A10:
Det (EqSegm (M,{I,J},{N,P})) = 0. K
by A1, A2, A3, Th96;
card {N,P} = 2
by A3, CARD_2:57;
then A11:
EqSegm (
M,
{I,J},
{N,P})
= Segm (
M,
{I,J},
{N,P})
by A9, Def3;
per cases
( ( I < J & N < P ) or ( I < J & N > P ) or ( I > J & N < P ) or ( I > J & N > P ) )
by A3, XXREAL_0:1;
suppose
(
I < J &
N < P )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))then 0. K =
Det (((M * (I,N)),(M * (I,P))) ][ ((M * (J,N)),(M * (J,P))))
by A9, A11, A10, Th45
.=
((M * (I,N)) * (M * (J,P))) - ((M * (I,P)) * (M * (J,N)))
by MATRIX_9:13
;
hence
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
by VECTSP_1:19;
verum end; suppose
(
I < J &
N > P )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))then 0. K =
Det (((M * (I,P)),(M * (I,N))) ][ ((M * (J,P)),(M * (J,N))))
by A9, A11, A10, Th45
.=
((M * (I,P)) * (M * (J,N))) - ((M * (I,N)) * (M * (J,P)))
by MATRIX_9:13
;
hence
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
by VECTSP_1:19;
verum end; suppose
(
I > J &
N < P )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))then 0. K =
Det (((M * (J,N)),(M * (J,P))) ][ ((M * (I,N)),(M * (I,P))))
by A9, A11, A10, Th45
.=
((M * (J,N)) * (M * (I,P))) - ((M * (J,P)) * (M * (I,N)))
by MATRIX_9:13
;
hence
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
by VECTSP_1:19;
verum end; suppose
(
I > J &
N > P )
;
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))then 0. K =
Det (((M * (J,P)),(M * (J,N))) ][ ((M * (I,P)),(M * (I,N))))
by A9, A11, A10, Th45
.=
((M * (J,P)) * (M * (I,N))) - ((M * (J,N)) * (M * (I,P)))
by MATRIX_9:13
;
hence
(M * (i,n)) * (M * (j,p)) = (M * (i,p)) * (M * (j,n))
by VECTSP_1:19;
verum end; end; end; end;
end;
assume that
A12:
ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K )
and
A13:
for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n))
; the_rank_of M = 1
now for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. Klet i0,
j0,
n0,
m0 be non
zero Nat;
( i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M implies Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K )assume that A14:
i0 <> j0
and A15:
n0 <> m0
and A16:
[:{i0,j0},{n0,m0}:] c= Indices M
;
Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. KA17:
card {i0,j0} = 2
by A14, CARD_2:57;
set JM =
M * (
j0,
m0);
set JN =
M * (
j0,
n0);
set IM =
M * (
i0,
m0);
set IN =
M * (
i0,
n0);
A18:
(M * (i0,n0)) * (M * (j0,m0)) = (M * (i0,m0)) * (M * (j0,n0))
by A13, A16;
card {n0,m0} = 2
by A15, CARD_2:57;
then A19:
EqSegm (
M,
{i0,j0},
{n0,m0})
= Segm (
M,
{i0,j0},
{n0,m0})
by A17, Def3;
per cases
( ( i0 < j0 & n0 < m0 ) or ( i0 < j0 & n0 > m0 ) or ( i0 > j0 & n0 < m0 ) or ( i0 > j0 & n0 > m0 ) )
by A14, A15, XXREAL_0:1;
suppose
(
i0 < j0 &
n0 < m0 )
;
Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. Kthen
EqSegm (
M,
{i0,j0},
{n0,m0})
= (
(M * (i0,n0)),
(M * (i0,m0)))
][ (
(M * (j0,n0)),
(M * (j0,m0)))
by A19, Th45;
hence Det (EqSegm (M,{i0,j0},{n0,m0})) =
((M * (i0,n0)) * (M * (j0,m0))) - ((M * (i0,m0)) * (M * (j0,n0)))
by A17, MATRIX_9:13
.=
0. K
by A18, VECTSP_1:19
;
verum end; suppose
(
i0 < j0 &
n0 > m0 )
;
Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. Kthen
EqSegm (
M,
{i0,j0},
{n0,m0})
= (
(M * (i0,m0)),
(M * (i0,n0)))
][ (
(M * (j0,m0)),
(M * (j0,n0)))
by A19, Th45;
hence Det (EqSegm (M,{i0,j0},{n0,m0})) =
((M * (i0,m0)) * (M * (j0,n0))) - ((M * (i0,n0)) * (M * (j0,m0)))
by A17, MATRIX_9:13
.=
0. K
by A18, VECTSP_1:19
;
verum end; suppose
(
i0 > j0 &
n0 < m0 )
;
Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. Kthen
EqSegm (
M,
{i0,j0},
{n0,m0})
= (
(M * (j0,n0)),
(M * (j0,m0)))
][ (
(M * (i0,n0)),
(M * (i0,m0)))
by A19, Th45;
hence Det (EqSegm (M,{i0,j0},{n0,m0})) =
((M * (j0,n0)) * (M * (i0,m0))) - ((M * (j0,m0)) * (M * (i0,n0)))
by A17, MATRIX_9:13
.=
0. K
by A18, VECTSP_1:19
;
verum end; suppose
(
i0 > j0 &
n0 > m0 )
;
Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. Kthen
EqSegm (
M,
{i0,j0},
{n0,m0})
= (
(M * (j0,m0)),
(M * (j0,n0)))
][ (
(M * (i0,m0)),
(M * (i0,n0)))
by A19, Th45;
hence Det (EqSegm (M,{i0,j0},{n0,m0})) =
((M * (j0,m0)) * (M * (i0,n0))) - ((M * (j0,n0)) * (M * (i0,m0)))
by A17, MATRIX_9:13
.=
0. K
by A18, VECTSP_1:19
;
verum end; end; end;
hence
the_rank_of M = 1
by A12, Th96; verum