let X be ComplexNormSpace; 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); f * (g + h) = (f * g) + (f * h)
set BLOP = C_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_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)),(C_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 fh =
(modetrans (f,X,X)) * (modetrans (h,X,X)) as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def 7;
reconsider fg =
(modetrans (f,X,X)) * (modetrans (g,X,X)) as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def 7;
reconsider k =
(modetrans (f,X,X)) * (modetrans ((g + h),X,X)) as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def 7;
reconsider hh =
h as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider gg =
g as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1:
(
gg = modetrans (
g,
X,
X) &
hh = modetrans (
h,
X,
X) )
by CLOPBAN1:def 9;
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;
((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)
(
g + h = gg + hh &
modetrans (
(g + h),
X,
X)
= g + h )
by CLOPBAN1:def 9;
then A2:
(modetrans ((g + h),X,X)) . x = ((modetrans (g,X,X)) . x) + ((modetrans (h,X,X)) . x)
by A1, CLOPBAN1:34;
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 A2, VECTSP_1:def 20
.=
(((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
;
verum
end;
then
k = fg + fh
by CLOPBAN1:34;
hence
(Add_ ((BoundedLinearOperators (X,X)),(C_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))
;
verum
end;
hence
f * (g + h) = (f * g) + (f * h)
; verum