let X be non empty set ; :: thesis: 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 upper_bound (PreNorms ONE) = 1 by SEQ_4:9;

then A6: ||.(1. B).|| = 1 by A1, A2, Th13;

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; :: thesis: verum

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 )

proof

then
PreNorms ONE = {1}
by TARSKI:def 1;
set t = the Element of X;

let s be object ; :: thesis: ( s in PreNorms ONE iff s = 1 )

A4: (X --> 1) . the Element of X = 1 ;

hence s in PreNorms ONE by A1, A3, A4, COMPLEX1:48; :: thesis: verum

end;let s be object ; :: thesis: ( s in PreNorms ONE iff s = 1 )

A4: (X --> 1) . the Element of X = 1 ;

hereby :: thesis: ( s = 1 implies s in PreNorms ONE )

assume
s = 1
; :: thesis: s in PreNorms ONEassume
s in PreNorms ONE
; :: thesis: s = 1

then consider t being Element of X such that

A5: s = |.(ONE . t).| ;

thus s = 1 by A5, COMPLEX1:48, A1, A3; :: thesis: verum

end;then consider t being Element of X such that

A5: s = |.(ONE . t).| ;

thus s = 1 by A5, COMPLEX1:48, A1, A3; :: thesis: verum

hence s in PreNorms ONE by A1, A3, A4, COMPLEX1:48; :: thesis: verum

then upper_bound (PreNorms ONE) = 1 by SEQ_4:9;

then A6: ||.(1. B).|| = 1 by A1, A2, Th13;

A7: now :: thesis: for a being Complex

for f, g being Element of B holds a * (f * g) = f * (a * g)

for f, g being Element of B holds a * (f * g) = f * (a * g)

let a be Complex; :: thesis: for f, g being Element of B holds a * (f * g) = f * (a * g)

let f, g be Element of B; :: thesis: 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 ;

end;let f, g be Element of B; :: thesis: 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 ;

now :: thesis: for x being Element of X holds h3 . x = (f1 . x) * (h1 . x)

hence
a * (f * g) = f * (a * g)
by A8, A12, A10, Th24; :: thesis: verumlet x be Element of X; :: thesis: h3 . x = (f1 . x) * (h1 . x)

h3 . x = a * (h2 . x) by A11, A10, Th23;

then h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th24;

then h3 . x = (f1 . x) * (a * (g1 . x)) ;

hence h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th23; :: thesis: verum

end;h3 . x = a * (h2 . x) by A11, A10, Th23;

then h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th24;

then h3 . x = (f1 . x) * (a * (g1 . x)) ;

hence h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th23; :: thesis: verum

A13: now :: thesis: for f, g being Element of B holds ||.(f * g).|| <= ||.f.|| * ||.g.||

let f, g be Element of B; :: thesis: ||.(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;

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; :: thesis: verum

end;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 :: thesis: for s being Real st s in PreNorms h1 holds

s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))

then A27:
upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by SEQ_4:45;s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))

let s be Real; :: thesis: ( s in PreNorms h1 implies s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) )

assume s in PreNorms h1 ; :: thesis: 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; :: thesis: verum

end;assume s in PreNorms h1 ; :: thesis: 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; :: thesis: verum

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; :: thesis: verum

A29: now :: thesis: for f, g, h being Element of B holds (g + h) * f = (g * f) + (h * f)

for f being Element of B holds (1. B) * f = f
by Lm3;let f, g, h be Element of B; :: thesis: (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 ;

end;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 :: thesis: for x being Element of X holds F1 . x = (gf1 . x) + (hf1 . x)

hence
(g + h) * f = (g * f) + (h * f)
by A35, A34, A33, Th22; :: thesis: verumlet x be Element of X; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum