let K be Field; for M being Matrix of K holds
( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )
let M be Matrix of K; ( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )
A1:
Indices M = [:(Seg (len M)),(Seg (width M)):]
by FINSEQ_1:def 3;
thus
( the_rank_of M = 1 implies ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )
( ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) implies the_rank_of M = 1 )proof
assume A2:
the_rank_of M = 1
;
ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) )
then consider i,
j being
Nat such that A3:
[i,j] in Indices M
and A4:
M * (
i,
j)
<> 0. K
by Th97;
take
i
;
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) )
A5:
j in Seg (width M)
by A3, ZFMISC_1:87;
hence
(
i in Seg (len M) & ex
j being
Nat st
(
j in Seg (width M) &
M * (
i,
j)
<> 0. K ) )
by A1, A3, A4, ZFMISC_1:87;
for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i))
set Li =
Line (
M,
i);
set ij =
M * (
i,
j);
let k be
Nat;
( k in Seg (len M) implies ex a being Element of K st Line (M,k) = a * (Line (M,i)) )
assume A6:
k in Seg (len M)
;
ex a being Element of K st Line (M,k) = a * (Line (M,i))
set Lk =
Line (
M,
k);
set kj =
M * (
k,
j);
take a =
(M * (k,j)) * ((M * (i,j)) ");
Line (M,k) = a * (Line (M,i))
A7:
i in Seg (len M)
by A1, A3, ZFMISC_1:87;
A8:
now for n being Nat st 1 <= n & n <= width M holds
(Line (M,k)) . n = (a * (Line (M,i))) . nlet n be
Nat;
( 1 <= n & n <= width M implies (Line (M,k)) . n = (a * (Line (M,i))) . n )assume that A9:
1
<= n
and A10:
n <= width M
;
(Line (M,k)) . n = (a * (Line (M,i))) . nA11:
n in Seg (width M)
by A9, A10;
then A12:
{j,n} c= Seg (width M)
by A5, ZFMISC_1:32;
(Line (M,i)) . n = M * (
i,
n)
by A11, MATRIX_0:def 7;
then A13:
(a * (Line (M,i))) . n = a * (M * (i,n))
by A11, FVSUM_1:51;
A14:
M * (
k,
j) =
(M * (k,j)) * (1_ K)
.=
(M * (k,j)) * ((M * (i,j)) * ((M * (i,j)) "))
by A4, VECTSP_1:def 10
.=
a * (M * (i,j))
by GROUP_1:def 3
;
{i,k} c= Seg (len M)
by A7, A6, ZFMISC_1:32;
then
[:{i,k},{j,n}:] c= Indices M
by A1, A12, ZFMISC_1:96;
then A15:
(M * (i,j)) * (M * (k,n)) =
(a * (M * (i,j))) * (M * (i,n))
by A2, A14, Th97
.=
(M * (i,j)) * (a * (M * (i,n)))
by GROUP_1:def 3
;
(Line (M,k)) . n = M * (
k,
n)
by A11, MATRIX_0:def 7;
hence
(Line (M,k)) . n = (a * (Line (M,i))) . n
by A4, A15, A13, VECTSP_2:8;
verum end;
A16:
len (a * (Line (M,i))) = width M
by CARD_1:def 7;
len (Line (M,k)) = width M
by CARD_1:def 7;
hence
Line (
M,
k)
= a * (Line (M,i))
by A16, A8;
verum
end;
given i being Nat such that A17:
i in Seg (len M)
and
A18:
ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K )
and
A19:
for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i))
; the_rank_of M = 1
A20:
now 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))set Li =
Line (
M,
i);
let I,
J,
n,
m be
Nat;
( [:{I,J},{n,m}:] c= Indices M implies (M * (I,n)) * (M * (J,m)) = (M * (I,m)) * (M * (J,n)) )assume A21:
[:{I,J},{n,m}:] c= Indices M
;
(M * (I,n)) * (M * (J,m)) = (M * (I,m)) * (M * (J,n))A22:
{n,m} c= Seg (width M)
by A21, ZFMISC_1:114;
then A23:
n in Seg (width M)
by ZFMISC_1:32;
then A24:
(Line (M,i)) . n = M * (
i,
n)
by MATRIX_0:def 7;
set LJ =
Line (
M,
J);
set LI =
Line (
M,
I);
A25:
{I,J} c= Seg (len M)
by A1, A21, ZFMISC_1:114;
then
I in Seg (len M)
by ZFMISC_1:32;
then consider a being
Element of
K such that A26:
Line (
M,
I)
= a * (Line (M,i))
by A19;
J in Seg (len M)
by A25, ZFMISC_1:32;
then consider b being
Element of
K such that A27:
Line (
M,
J)
= b * (Line (M,i))
by A19;
(Line (M,J)) . n = M * (
J,
n)
by A23, MATRIX_0:def 7;
then A28:
M * (
J,
n)
= b * (M * (i,n))
by A27, A23, A24, FVSUM_1:51;
A29:
m in Seg (width M)
by A22, ZFMISC_1:32;
then A30:
(Line (M,i)) . m = M * (
i,
m)
by MATRIX_0:def 7;
(Line (M,J)) . m = M * (
J,
m)
by A29, MATRIX_0:def 7;
then A31:
M * (
J,
m)
= b * (M * (i,m))
by A27, A29, A30, FVSUM_1:51;
(Line (M,I)) . m = M * (
I,
m)
by A29, MATRIX_0:def 7;
then A32:
M * (
I,
m)
= a * (M * (i,m))
by A26, A29, A30, FVSUM_1:51;
(Line (M,I)) . n = M * (
I,
n)
by A23, MATRIX_0:def 7;
then
M * (
I,
n)
= a * (M * (i,n))
by A26, A23, A24, FVSUM_1:51;
hence (M * (I,n)) * (M * (J,m)) =
((a * (M * (i,n))) * b) * (M * (i,m))
by A31, GROUP_1:def 3
.=
((b * (M * (i,n))) * a) * (M * (i,m))
by GROUP_1:def 3
.=
(M * (I,m)) * (M * (J,n))
by A28, A32, GROUP_1:def 3
;
verum end;
consider j being Nat such that
A33:
j in Seg (width M)
and
A34:
M * (i,j) <> 0. K
by A18;
[i,j] in Indices M
by A1, A17, A33, ZFMISC_1:87;
hence
the_rank_of M = 1
by A34, A20, Th97; verum