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