let X be RealNormSpace; :: thesis: for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let f, g be Element of BoundedLinearOperators (X,X); :: thesis: for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let a, b be Real; :: thesis: (a * b) * (f * g) = (a * f) * (b * g)
set BLOP = R_NormSpace_of_BoundedLinearOperators (X,X);
set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(R_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)),(R_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 k = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;
reconsider ff = f, gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: gg = modetrans (g,X,X) by LOPBAN_1:def 11;
A2: ff = modetrans (f,X,X) by LOPBAN_1:def 11;
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);
( a * f = a * ff & modetrans ((a * f),X,X) = a * f ) by LOPBAN_1:def 11;
then A3: (modetrans ((a * f),X,X)) . (b * ((modetrans (g,X,X)) . x)) = a * ((modetrans (f,X,X)) . (b * ((modetrans (g,X,X)) . x))) by A2, LOPBAN_1:36;
( b * g = b * gg & modetrans ((b * g),X,X) = b * g ) by LOPBAN_1:def 11;
then A4: (modetrans ((b * g),X,X)) . x = b * ((modetrans (g,X,X)) . x) by A1, LOPBAN_1:36;
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 A3, A4, LOPBAN_1:def 5
.= (a * b) * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) by RLVECT_1:def 7
.= (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) by Th4 ; :: thesis: verum

end;

then k = (a * b) * fg by LOPBAN_1:36;
hence (Mult_ ((BoundedLinearOperators (X,X)),(R_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