let n be Nat; for M1, M2 being Matrix of n,REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
let M1, M2 be Matrix of n,REAL; |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
A1:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A2:
Indices (M1 + M2) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A3:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices |:(M1 + M2):| holds
|:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices |:(M1 + M2):| implies |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) )
assume
[i,j] in Indices |:(M1 + M2):|
;
|:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j)
then A4:
[i,j] in Indices (M1 + M2)
by Th5;
then
[i,j] in Indices |:M1:|
by A1, A2, Th5;
then A5:
(|:M1:| + |:M2:|) * (
i,
j) =
(|:M1:| * (i,j)) + (|:M2:| * (i,j))
by MATRIXR1:25
.=
|.(M1 * (i,j)).| + (|:M2:| * (i,j))
by A1, A2, A4, Def7
.=
|.(M1 * (i,j)).| + |.(M2 * (i,j)).|
by A3, A2, A4, Def7
;
|:(M1 + M2):| * (
i,
j) =
|.((M1 + M2) * (i,j)).|
by A4, Def7
.=
|.((M1 * (i,j)) + (M2 * (i,j))).|
by A1, A2, A4, MATRIXR1:25
;
hence
|:(M1 + M2):| * (
i,
j)
<= (|:M1:| + |:M2:|) * (
i,
j)
by A5, COMPLEX1:56;
verum
end;
hence
|:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
; verum