set NRM = BoundedLinearOperatorsNorm (X,X);
set UNIT = FuncUnit X;
set MULT = FuncMult X;
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set BS = C_NormSpace_of_BoundedLinearOperators (X,X);
set BLOP = BoundedLinearOperators (X,X);
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
thus
C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1
CLOPBAN2:def 12 ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )proof
let x,
y be
Point of
(C_Normed_Algebra_of_BoundedLinearOperators X);
CLOPBAN2:def 9 ||.(x * y).|| <= ||.x.|| * ||.y.||
reconsider x1 =
x,
y1 =
y as
Element of
BoundedLinearOperators (
X,
X) ;
A1:
((BoundedLinearOperatorsNorm (X,X)) . (modetrans (x1,X,X))) * ((BoundedLinearOperatorsNorm (X,X)) . (modetrans (y1,X,X))) =
((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . (modetrans (y1,X,X)))
by CLOPBAN1:def 9
.=
||.x.|| * ||.y.||
by CLOPBAN1:def 9
;
||.(x * y).|| =
(BoundedLinearOperatorsNorm (X,X)) . (x1 * y1)
by Def4
.=
(BoundedLinearOperatorsNorm (X,X)) . ((modetrans (x1,X,X)) * (modetrans (y1,X,X)))
;
hence
||.(x * y).|| <= ||.x.|| * ||.y.||
by A1, Th2;
verum
end;
||.(1. (C_Normed_Algebra_of_BoundedLinearOperators X)).|| = 1
by Th18;
hence
C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2
; ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus
C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3
( C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus
C_Normed_Algebra_of_BoundedLinearOperators X is left_unital
( C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus
C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive
C_Normed_Algebra_of_BoundedLinearOperators X is complete proof
let x,
y,
z be
Element of
(C_Normed_Algebra_of_BoundedLinearOperators X);
VECTSP_1:def 3 (y + z) * x = (y * x) + (z * x)
reconsider xx =
x,
yy =
y,
zz =
z as
Element of
BoundedLinearOperators (
X,
X) ;
thus (y + z) * x =
(yy + zz) * xx
by Def4
.=
(yy * xx) + (zz * xx)
by Th10
.=
(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (
(yy * xx),
((FuncMult X) . (zz,xx)))
by Def4
.=
(y * x) + (z * x)
by Def4
;
verum
end;
hence
C_Normed_Algebra_of_BoundedLinearOperators X is complete
; verum