let K be Field; for M being Matrix of K holds
( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )
let M be Matrix of K; ( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )
set NULL = 0. (K,(len M),(width M));
reconsider M9 = M as Matrix of len M, width M,K by MATRIX_0:51;
thus
( the_rank_of M = 0 implies M = 0. (K,(len M),(width M)) )
( M = 0. (K,(len M),(width M)) implies the_rank_of M = 0 )proof
assume A1:
the_rank_of M = 0
;
M = 0. (K,(len M),(width M))
now for i, j being Nat st [i,j] in Indices M9 holds
M9 * (i,j) = (0. (K,(len M),(width M))) * (i,j)A2:
Indices M9 = Indices (0. (K,(len M),(width M)))
by MATRIX_0:26;
let i,
j be
Nat;
( [i,j] in Indices M9 implies M9 * (i,j) = (0. (K,(len M),(width M))) * (i,j) )assume A3:
[i,j] in Indices M9
;
M9 * (i,j) = (0. (K,(len M),(width M))) * (i,j)reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
M * (
i9,
j9)
= 0. K
by A1, A3, Th94;
hence
M9 * (
i,
j)
= (0. (K,(len M),(width M))) * (
i,
j)
by A3, A2, MATRIX_3:1;
verum end;
hence
M = 0. (
K,
(len M),
(width M))
by MATRIX_0:27;
verum
end;
assume A4:
M = 0. (K,(len M),(width M))
; the_rank_of M = 0
assume
the_rank_of M <> 0
; contradiction
then
ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K )
by Th94;
hence
contradiction
by A4, MATRIX_3:1; verum