let X be non empty set ; C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra
set B = C_Normed_Algebra_of_BoundedFunctions X;
reconsider B = C_Normed_Algebra_of_BoundedFunctions X as Normed_Complex_Algebra by Th15;
set X1 = ComplexBoundedFunctions X;
1. B in ComplexBoundedFunctions X
;
then consider ONE being Function of X,COMPLEX such that
A1:
ONE = 1. B
and
A2:
ONE | X is bounded
;
1. B = 1_ (C_Algebra_of_BoundedFunctions X)
;
then A3:
1. B = X --> 1r
by Th9;
for s being object holds
( s in PreNorms ONE iff s = 1 )
then
PreNorms ONE = {1}
by TARSKI:def 1;
then
upper_bound (PreNorms ONE) = 1
by SEQ_4:9;
then A6:
||.(1. B).|| = 1
by A1, A2, Th13;
A7:
now for a being Complex
for f, g being Element of B holds a * (f * g) = f * (a * g)let a be
Complex;
for f, g being Element of B holds a * (f * g) = f * (a * g)let f,
g be
Element of
B;
a * (f * g) = f * (a * g)
f in ComplexBoundedFunctions X
;
then consider f1 being
Function of
X,
COMPLEX such that A8:
f1 = f
and
f1 | X is
bounded
;
g in ComplexBoundedFunctions X
;
then consider g1 being
Function of
X,
COMPLEX such that A9:
g1 = g
and
g1 | X is
bounded
;
a * (f * g) in ComplexBoundedFunctions X
;
then consider h3 being
Function of
X,
COMPLEX such that A10:
h3 = a * (f * g)
and
h3 | X is
bounded
;
f * g in ComplexBoundedFunctions X
;
then consider h2 being
Function of
X,
COMPLEX such that A11:
h2 = f * g
and
h2 | X is
bounded
;
a * g in ComplexBoundedFunctions X
;
then consider h1 being
Function of
X,
COMPLEX such that A12:
h1 = a * g
and
h1 | X is
bounded
;
hence
a * (f * g) = f * (a * g)
by A8, A12, A10, Th24;
verum end;
A13:
now for f, g being Element of B holds ||.(f * g).|| <= ||.f.|| * ||.g.||let f,
g be
Element of
B;
||.(f * g).|| <= ||.f.|| * ||.g.||
f in ComplexBoundedFunctions X
;
then consider f1 being
Function of
X,
COMPLEX such that A14:
f1 = f
and A15:
f1 | X is
bounded
;
g in ComplexBoundedFunctions X
;
then consider g1 being
Function of
X,
COMPLEX such that A16:
g1 = g
and A17:
g1 | X is
bounded
;
A18:
( not
PreNorms g1 is
empty &
PreNorms g1 is
bounded_above )
by A17, Th10;
f * g in ComplexBoundedFunctions X
;
then consider h1 being
Function of
X,
COMPLEX such that A19:
h1 = f * g
and A20:
h1 | X is
bounded
;
A21:
( not
PreNorms f1 is
empty &
PreNorms f1 is
bounded_above )
by A15, Th10;
now for s being Real st s in PreNorms h1 holds
s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))let s be
Real;
( s in PreNorms h1 implies s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) )assume
s in PreNorms h1
;
s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))then consider t being
Element of
X such that A22:
s = |.(h1 . t).|
;
|.(g1 . t).| in PreNorms g1
;
then A23:
|.(g1 . t).| <= upper_bound (PreNorms g1)
by A18, SEQ_4:def 1;
|.(f1 . t).| in PreNorms f1
;
then A24:
|.(f1 . t).| <= upper_bound (PreNorms f1)
by A21, SEQ_4:def 1;
then A25:
(upper_bound (PreNorms f1)) * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by A23, XREAL_1:64;
A26:
|.(f1 . t).| * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * |.(g1 . t).|
by A24, XREAL_1:64;
|.(h1 . t).| = |.((f1 . t) * (g1 . t)).|
by A14, A16, A19, Th24;
then
|.(h1 . t).| = |.(f1 . t).| * |.(g1 . t).|
by COMPLEX1:65;
hence
s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by A22, A26, A25, XXREAL_0:2;
verum end; then A27:
upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by SEQ_4:45;
A28:
||.g.|| = upper_bound (PreNorms g1)
by A16, A17, Th13;
||.f.|| = upper_bound (PreNorms f1)
by A14, A15, Th13;
hence
||.(f * g).|| <= ||.f.|| * ||.g.||
by A19, A20, A28, A27, Th13;
verum end;
A29:
now for f, g, h being Element of B holds (g + h) * f = (g * f) + (h * f)let f,
g,
h be
Element of
B;
(g + h) * f = (g * f) + (h * f)
f in ComplexBoundedFunctions X
;
then consider f1 being
Function of
X,
COMPLEX such that A30:
f1 = f
and
f1 | X is
bounded
;
h in ComplexBoundedFunctions X
;
then consider h1 being
Function of
X,
COMPLEX such that A31:
h1 = h
and
h1 | X is
bounded
;
g in ComplexBoundedFunctions X
;
then consider g1 being
Function of
X,
COMPLEX such that A32:
g1 = g
and
g1 | X is
bounded
;
(g + h) * f in ComplexBoundedFunctions X
;
then consider F1 being
Function of
X,
COMPLEX such that A33:
F1 = (g + h) * f
and
F1 | X is
bounded
;
h * f in ComplexBoundedFunctions X
;
then consider hf1 being
Function of
X,
COMPLEX such that A34:
hf1 = h * f
and
hf1 | X is
bounded
;
g * f in ComplexBoundedFunctions X
;
then consider gf1 being
Function of
X,
COMPLEX such that A35:
gf1 = g * f
and
gf1 | X is
bounded
;
g + h in ComplexBoundedFunctions X
;
then consider gPh1 being
Function of
X,
COMPLEX such that A36:
gPh1 = g + h
and
gPh1 | X is
bounded
;
now for x being Element of X holds F1 . x = (gf1 . x) + (hf1 . x)let x be
Element of
X;
F1 . x = (gf1 . x) + (hf1 . x)
F1 . x = (gPh1 . x) * (f1 . x)
by A30, A36, A33, Th24;
then
F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x)
by A32, A31, A36, Th22;
then
F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x))
;
then
F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x))
by A30, A32, A35, Th24;
hence
F1 . x = (gf1 . x) + (hf1 . x)
by A30, A31, A34, Th24;
verum end; hence
(g + h) * f = (g * f) + (h * f)
by A35, A34, A33, Th22;
verum end;
for f being Element of B holds (1. B) * f = f
by Lm3;
then A37:
B is left_unital
;
A38:
B is Banach_Algebra-like_1
by A13, CLOPBAN2:def 9;
A39:
B is Banach_Algebra-like_2
by A6, CLOPBAN2:def 10;
A40:
B is Banach_Algebra-like_3
by A7, CLOPBAN2:def 11;
B is left-distributive
by A29;
hence
C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra
by A37, A38, A39, A40; verum