let X, Y, Z be RealNormSpace; for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )
let w be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); ( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )
A2:
modetrans (u,X,Y) = u
by LOPBAN_1:def 11;
for x being Point of X holds (w * (u - v)) . x = ((w * u) . x) - ((w * v) . x)
proof
let x be
Point of
X;
(w * (u - v)) . x = ((w * u) . x) - ((w * v) . x)
A6:
modetrans (
w,
Y,
Z) is
additive
;
thus (w * (u - v)) . x =
(modetrans (w,Y,Z)) . ((modetrans ((u - v),X,Y)) . x)
by FUNCT_2:15
.=
(modetrans (w,Y,Z)) . ((u - v) . x)
by LOPBAN_1:def 11
.=
(modetrans (w,Y,Z)) . ((u . x) - (v . x))
by LOPBAN_1:40
.=
((modetrans (w,Y,Z)) . (u . x)) + ((modetrans (w,Y,Z)) . (- (v . x)))
by A6
.=
((modetrans (w,Y,Z)) . (u . x)) + ((modetrans (w,Y,Z)) . ((- 1) * (v . x)))
by RLVECT_1:16
.=
((modetrans (w,Y,Z)) . (u . x)) + ((- 1) * ((modetrans (w,Y,Z)) . (v . x)))
by LOPBAN_1:def 5
.=
((modetrans (w,Y,Z)) . (u . x)) - ((modetrans (w,Y,Z)) . (v . x))
by RLVECT_1:16
.=
((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) - ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x))
by A2, LOPBAN_1:def 11
.=
(((modetrans (w,Y,Z)) * (modetrans (u,X,Y))) . x) - ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x))
by FUNCT_2:15
.=
((w * u) . x) - ((w * v) . x)
by FUNCT_2:15
;
verum
end;
hence
w * (u - v) = (w * u) - (w * v)
by LOPBAN_1:40; w * (u + v) = (w * u) + (w * v)
for x being Point of X holds (w * (u + v)) . x = ((w * u) . x) + ((w * v) . x)
proof
let x be
Point of
X;
(w * (u + v)) . x = ((w * u) . x) + ((w * v) . x)
A7:
modetrans (
w,
Y,
Z) is
additive
;
thus (w * (u + v)) . x =
(modetrans (w,Y,Z)) . ((modetrans ((u + v),X,Y)) . x)
by FUNCT_2:15
.=
(modetrans (w,Y,Z)) . ((u + v) . x)
by LOPBAN_1:def 11
.=
(modetrans (w,Y,Z)) . ((u . x) + (v . x))
by LOPBAN_1:35
.=
((modetrans (w,Y,Z)) . (u . x)) + ((modetrans (w,Y,Z)) . (v . x))
by A7
.=
((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) + ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x))
by A2, LOPBAN_1:def 11
.=
(((modetrans (w,Y,Z)) * (modetrans (u,X,Y))) . x) + ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x))
by FUNCT_2:15
.=
((w * u) . x) + ((w * v) . x)
by FUNCT_2:15
;
verum
end;
hence
w * (u + v) = (w * u) + (w * v)
by LOPBAN_1:35; verum