let K be Field; :: thesis: 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; :: thesis: ( 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)) ) ) ) :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( [:{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 ; :: thesis: (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 ) ; :: thesis: (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)) ; :: thesis: verum
end;
suppose A3: ( i <> j & n <> p ) ; :: thesis: (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 ) ; :: thesis: (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; :: thesis: verum
end;
suppose ( I < J & N > P ) ; :: thesis: (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; :: thesis: verum
end;
suppose ( I > J & N < P ) ; :: thesis: (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; :: thesis: verum
end;
suppose ( I > J & N > P ) ; :: thesis: (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; :: thesis: 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)) ; :: thesis: the_rank_of M = 1
now :: thesis: 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. K
let i0, j0, n0, m0 be non zero Nat; :: thesis: ( 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 ; :: thesis: Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K
A17: 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 ) ; :: thesis: Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K
then 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 ;
:: thesis: verum
end;
suppose ( i0 < j0 & n0 > m0 ) ; :: thesis: Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K
then 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 ;
:: thesis: verum
end;
suppose ( i0 > j0 & n0 < m0 ) ; :: thesis: Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K
then 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 ;
:: thesis: verum
end;
suppose ( i0 > j0 & n0 > m0 ) ; :: thesis: Det (EqSegm (M,{b1,b2},{b3,b4})) = 0. K
then 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 ;
:: thesis: verum
end;
end;
end;
hence the_rank_of M = 1 by A12, Th96; :: thesis: verum