let X be RealNormSpace; :: thesis: for f, g, h being Element of BoundedLinearOperators X,X holds f * (g + h) = (f * g) + (f * h)
let f, g, h be Element of BoundedLinearOperators X,X; :: thesis: f * (g + h) = (f * g) + (f * h)
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 f,X,X) * (modetrans g,X,X)),((modetrans f,X,X) * (modetrans h,X,X)) = (modetrans f,X,X) * (modetrans (g + h),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 f,X,X) * (modetrans (g + h),X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider fg =
(modetrans f,X,X) * (modetrans g,X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider fh =
(modetrans f,X,X) * (modetrans h,X,X) as
VECTOR of
(R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
for
x being
VECTOR of
X holds
((modetrans f,X,X) * (modetrans (g + h),X,X)) . x = (((modetrans f,X,X) * (modetrans g,X,X)) . x) + (((modetrans f,X,X) * (modetrans h,X,X)) . x)
proof
let x be
VECTOR of
X;
:: thesis: ((modetrans f,X,X) * (modetrans (g + h),X,X)) . x = (((modetrans f,X,X) * (modetrans g,X,X)) . x) + (((modetrans f,X,X) * (modetrans h,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) . x = ((modetrans g,X,X) . x) + ((modetrans h,X,X) . x)
by A1, A2, A3, LOPBAN_1:41;
thus ((modetrans f,X,X) * (modetrans (g + h),X,X)) . x =
(modetrans f,X,X) . ((modetrans (g + h),X,X) . x)
by Th4
.=
((modetrans f,X,X) . ((modetrans g,X,X) . x)) + ((modetrans f,X,X) . ((modetrans h,X,X) . x))
by A4, LOPBAN_1:def 5
.=
(((modetrans f,X,X) * (modetrans g,X,X)) . x) + ((modetrans f,X,X) . ((modetrans h,X,X) . x))
by Th4
.=
(((modetrans f,X,X) * (modetrans g,X,X)) . x) + (((modetrans f,X,X) * (modetrans h,X,X)) . x)
by Th4
;
:: thesis: verum
end;
then
k = fg + fh
by LOPBAN_1:41;
hence
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . ((modetrans f,X,X) * (modetrans g,X,X)),
((modetrans f,X,X) * (modetrans h,X,X)) = (modetrans f,X,X) * (modetrans (g + h),X,X)
;
:: thesis: verum
end;
hence
f * (g + h) = (f * g) + (f * h)
; :: thesis: verum