let n be Nat; :: thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds
M1 + M4 is_less_or_equal_with M3 - M2
let M1, M2, M3, M4 be Matrix of n, REAL ; :: thesis: ( M1 + M2 is_less_or_equal_with M3 - M4 implies M1 + M4 is_less_or_equal_with M3 - M2 )
assume A1:
M1 + M2 is_less_or_equal_with M3 - M4
; :: thesis: M1 + M4 is_less_or_equal_with M3 - M2
A2:
( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] & Indices M3 = [:(Seg n),(Seg n):] & Indices M4 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] & Indices (M1 + M4) = [:(Seg n),(Seg n):] & Indices (M3 - M2) = [:(Seg n),(Seg n):] & Indices (M3 - M4) = [:(Seg n),(Seg n):] )
by MATRIX_1:25;
A3:
( len M3 = len M4 & width M3 = width M4 & len M2 = len M3 & width M2 = width M3 & len M1 = len M3 & width M1 = width M3 )
by Lm1;
for i, j being Nat st [i,j] in Indices (M1 + M4) holds
(M1 + M4) * i,j <= (M3 - M2) * i,j
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in Indices (M1 + M4) implies (M1 + M4) * i,j <= (M3 - M2) * i,j )
assume A4:
[i,j] in Indices (M1 + M4)
;
:: thesis: (M1 + M4) * i,j <= (M3 - M2) * i,j
then
(M1 + M2) * i,
j <= (M3 - M4) * i,
j
by A1, A2, Def6;
then
(M1 * i,j) + (M2 * i,j) <= (M3 - M4) * i,
j
by A2, A4, MATRIXR1:25;
then
(M1 * i,j) + (M2 * i,j) <= (M3 * i,j) - (M4 * i,j)
by A2, A3, A4, Th3;
then
(M1 * i,j) + (M4 * i,j) <= (M3 * i,j) - (M2 * i,j)
by XREAL_1:24;
then
(M1 + M4) * i,
j <= (M3 * i,j) - (M2 * i,j)
by A2, A4, MATRIXR1:25;
hence
(M1 + M4) * i,
j <= (M3 - M2) * i,
j
by A2, A3, A4, Th3;
:: thesis: verum
end;
hence
M1 + M4 is_less_or_equal_with M3 - M2
by Def6; :: thesis: verum