let X be RealNormSpace; :: thesis: for f, g, h being Element of BoundedLinearOperators X,X holds (g + h) * f = (g * f) + (h * f)
let f, g, h be Element of BoundedLinearOperators X,X; :: thesis: (g + h) * f = (g * f) + (h * f)
set BLOP = R_NormSpace_of_BoundedLinearOperators X,X;
set ADD = Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X);
set mf = modetrans f,X,X;
set mg = modetrans g,X,X;
set mh = modetrans h,X,X;
set mgh = modetrans (g + h),X,X;
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . ((modetrans g,X,X) * (modetrans f,X,X)),((modetrans h,X,X) * (modetrans f,X,X)) = (modetrans (g + h),X,X) * (modetrans f,X,X)
proof
reconsider gg =
g as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) ;
reconsider hh =
h as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) ;
A1:
gg = modetrans g,
X,
X
by LOPBAN_1:def 12;
A2:
hh = modetrans h,
X,
X
by LOPBAN_1:def 12;
reconsider k =
(modetrans (g + h),X,X) * (modetrans f,X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider gf =
(modetrans g,X,X) * (modetrans f,X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider hf =
(modetrans h,X,X) * (modetrans f,X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
for
x being
VECTOR of
X holds
((modetrans (g + h),X,X) * (modetrans f,X,X)) . x = (((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x)
proof
let x be
VECTOR of
X;
:: thesis: ((modetrans (g + h),X,X) * (modetrans f,X,X)) . x = (((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x)
A3:
g + h = gg + hh
;
modetrans (g + h),
X,
X = g + h
by LOPBAN_1:def 12;
then A4:
(modetrans (g + h),X,X) . ((modetrans f,X,X) . x) = ((modetrans g,X,X) . ((modetrans f,X,X) . x)) + ((modetrans h,X,X) . ((modetrans f,X,X) . x))
by A1, A2, A3, LOPBAN_1:41;
thus ((modetrans (g + h),X,X) * (modetrans f,X,X)) . x =
(modetrans (g + h),X,X) . ((modetrans f,X,X) . x)
by Th4
.=
(((modetrans g,X,X) * (modetrans f,X,X)) . x) + ((modetrans h,X,X) . ((modetrans f,X,X) . x))
by A4, Th4
.=
(((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x)
by Th4
;
:: thesis: verum
end;
then
k = gf + hf
by LOPBAN_1:41;
hence
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . ((modetrans g,X,X) * (modetrans f,X,X)),
((modetrans h,X,X) * (modetrans f,X,X)) = (modetrans (g + h),X,X) * (modetrans f,X,X)
;
:: thesis: verum
end;
hence
(g + h) * f = (g * f) + (h * f)
; :: thesis: verum