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