let X be ComplexNormSpace; :: thesis: for f, g being Element of BoundedLinearOperators X,X
for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)
let f, g be Element of BoundedLinearOperators X,X; :: thesis: for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)
let a, b be Complex; :: thesis: (a * b) * (f * g) = (a * f) * (b * g)
set BLOP = C_NormSpace_of_BoundedLinearOperators X,X;
set EXMULT = Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X);
set mf = modetrans f,X,X;
set mg = modetrans g,X,X;
set maf = modetrans (a * f),X,X;
set mbg = modetrans (b * g),X,X;
(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (a * b),((modetrans f,X,X) * (modetrans g,X,X)) = (modetrans (a * f),X,X) * (modetrans (b * g),X,X)
proof
reconsider ff =
f,
gg =
g as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators X,X) ;
A1:
ff = modetrans f,
X,
X
by CLOPBAN1:def 10;
A2:
gg = modetrans g,
X,
X
by CLOPBAN1:def 10;
reconsider fg =
(modetrans f,X,X) * (modetrans g,X,X) as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators X,X) by CLOPBAN1:def 8;
reconsider k =
(modetrans (a * f),X,X) * (modetrans (b * g),X,X) as
VECTOR of
(C_NormSpace_of_BoundedLinearOperators X,X) by CLOPBAN1:def 8;
for
x being
VECTOR of
X holds
((modetrans (a * f),X,X) * (modetrans (b * g),X,X)) . x = (a * b) * (((modetrans f,X,X) * (modetrans g,X,X)) . x)
proof
let x be
VECTOR of
X;
:: thesis: ((modetrans (a * f),X,X) * (modetrans (b * g),X,X)) . x = (a * b) * (((modetrans f,X,X) * (modetrans g,X,X)) . x)
set y =
b * ((modetrans g,X,X) . x);
A3:
a * f = a * ff
;
modetrans (a * f),
X,
X = a * f
by CLOPBAN1:def 10;
then A4:
(modetrans (a * f),X,X) . (b * ((modetrans g,X,X) . x)) = a * ((modetrans f,X,X) . (b * ((modetrans g,X,X) . x)))
by A1, A3, CLOPBAN1:40;
A5:
b * g = b * gg
;
modetrans (b * g),
X,
X = b * g
by CLOPBAN1:def 10;
then A6:
(modetrans (b * g),X,X) . x = b * ((modetrans g,X,X) . x)
by A2, A5, CLOPBAN1:40;
thus ((modetrans (a * f),X,X) * (modetrans (b * g),X,X)) . x =
(modetrans (a * f),X,X) . ((modetrans (b * g),X,X) . x)
by Th4
.=
a * (b * ((modetrans f,X,X) . ((modetrans g,X,X) . x)))
by A4, A6, CLOPBAN1:def 4
.=
(a * b) * ((modetrans f,X,X) . ((modetrans g,X,X) . x))
by CLVECT_1:def 2
.=
(a * b) * (((modetrans f,X,X) * (modetrans g,X,X)) . x)
by Th4
;
:: thesis: verum
end;
then
k = (a * b) * fg
by CLOPBAN1:40;
hence
(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (a * b),
((modetrans f,X,X) * (modetrans g,X,X)) = (modetrans (a * f),X,X) * (modetrans (b * g),X,X)
;
:: thesis: verum
end;
hence
(a * b) * (f * g) = (a * f) * (b * g)
; :: thesis: verum