let n, m be Nat; for K being Ring
for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
let K be Ring; for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
let A be Matrix of n,m,K; A + (- A) = 0. (K,n,m)
A1:
width (- A) = width A
by Def2;
A2:
len (A + (- A)) = len A
by Def3;
A3:
width (A + (- A)) = width A
by Def3;
A4:
len (- A) = len A
by Def2;
A5:
now ( ( n > 0 & len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) or ( n = 0 & len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) )per cases
( n > 0 or n = 0 )
;
case A6:
n > 0
;
( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )then
(
len (A + (- A)) = n &
width (A + (- A)) = m )
by A2, A3, MATRIX_0:23;
hence
(
len (0. (K,n,m)) = len (A + (- A)) &
width (0. (K,n,m)) = width (A + (- A)) )
by A6, MATRIX_0:23;
( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
(
dom A = dom (- A) &
dom A = dom (A + (- A)) )
by A4, A2, FINSEQ_3:29;
hence
(
Indices A = Indices (- A) &
Indices A = Indices (A + (- A)) )
by A1, A3;
verum end; case A7:
n = 0
;
( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )then A8:
width A = 0
by MATRIX_0:22;
then A9:
Seg (width (- A)) = Seg 0
by A1;
A10:
len A = 0
by A7, MATRIX_0:22;
then A11:
dom (- A) = Seg 0
by A4, FINSEQ_1:def 3;
A12:
Indices (- A) =
[:(dom (- A)),(Seg (width (- A))):]
.=
[:(Seg 0),(Seg (width (- A))):]
by A11
.=
[:(Seg 0),(Seg 0):]
by A9
;
dom (A + (- A)) = Seg 0
by A2, A10, FINSEQ_1:def 3;
then A13:
Indices (A + (- A)) = [:(Seg 0),(Seg 0):]
by A3, A8;
(
len (0. (K,n,m)) = 0 &
width (0. (K,n,m)) = 0 )
by A7, MATRIX_0:22;
hence
(
len (0. (K,n,m)) = len (A + (- A)) &
width (0. (K,n,m)) = width (A + (- A)) )
by A10, A8, Def3;
( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
Indices A = {}
by A7, MATRIX_0:22;
hence
(
Indices A = Indices (- A) &
Indices A = Indices (A + (- A)) )
by A12, A13, ZFMISC_1:90;
verum end;
A14:
Indices A = Indices (0. (K,n,m))
by MATRIX_0:26;
now for i, j being Nat st [i,j] in Indices A holds
(A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j)let i,
j be
Nat;
( [i,j] in Indices A implies (A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j) )assume A15:
[i,j] in Indices A
;
(A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j)hence (A + (- A)) * (
i,
j) =
(A * (i,j)) + ((- A) * (i,j))
by Def3
.=
(A * (i,j)) + (- (A * (i,j)))
by A15, Def2
.=
0. K
by RLVECT_1:5
.=
(0. (K,n,m)) * (
i,
j)
by A14, A15, Th1
;
verum end;
hence
A + (- A) = 0. (K,n,m)
by A5, MATRIX_0:21; verum