let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K holds
( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
let K be Field; :: thesis: for A being Matrix of n,K holds
( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
let A be Matrix of n,K; :: thesis: ( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
thus
( A = 0. K,n implies for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
:: thesis: ( ( for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K ) implies A = 0. K,n )proof
assume B1:
A = 0. K,
n
;
:: thesis: for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K
let i,
j be
Element of
NAT ;
:: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies A * i,j = 0. K )
assume C1:
( 1
<= i &
i <= n & 1
<= j &
j <= n )
;
:: thesis: A * i,j = 0. K
set A3 =
0. K,
n,
n;
reconsider B3 =
0. K,
n,
n as
Matrix of
n,
K ;
set A2 =
0. K,
n;
set B2 =
0. K,
n;
C3:
(
0. K,
n,
n = 0. K,
n &
B3 = 0. K,
n &
A = 0. K,
n &
0. K,
n = A )
by B1, MATRIX_3:def 1;
C6:
[i,j] in Indices (0. K,n)
by C1, MATRIX_1:38;
C7:
((0. K,n) + (0. K,n)) * i,
j = ((0. K,n) * i,j) + ((0. K,n) * i,j)
by C6, MATRIX_3:def 3;
C8:
(0. K,n) * i,
j = ((0. K,n) * i,j) + ((0. K,n) * i,j)
by C3, C7, MATRIX_3:6;
((0. K,n) * i,j) - ((0. K,n) * i,j) =
((0. K,n) * i,j) + (((0. K,n) * i,j) - ((0. K,n) * i,j))
by C8, RLVECT_1:42
.=
((0. K,n) * i,j) + (0. K)
by RLVECT_1:28
.=
(0. K,n) * i,
j
by RLVECT_1:10
;
hence
A * i,
j = 0. K
by B1, RLVECT_1:28;
:: thesis: verum
end;
assume B1:
for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K
; :: thesis: A = 0. K,n
B2:
( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] )
by MATRIX_1:25;
for i, j being Nat st [i,j] in Indices A holds
A * i,j = (A * i,j) + (A * i,j)
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in Indices A implies A * i,j = (A * i,j) + (A * i,j) )
assume
[i,j] in Indices A
;
:: thesis: A * i,j = (A * i,j) + (A * i,j)
then
(
i in Seg n &
j in Seg n )
by B2, ZFMISC_1:106;
then C2:
( 1
<= i &
i <= n & 1
<= j &
j <= n )
by FINSEQ_1:3;
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
A * i0,
j0 = 0. K
by B1, C2;
hence
A * i,
j = (A * i,j) + (A * i,j)
by RLVECT_1:10;
:: thesis: verum
end;
then B4:
A = A + A
by B2, MATRIX_3:def 3;
A = 0. K,(len A),(width A)
by B4, MATRIX_4:6;
hence
A = 0. K,n
by B2, MATRIX_3:def 1; :: thesis: verum