let X be non empty set ; :: thesis:
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_ ;
then A3: 1. B = X --> 1r by Th9;
for s being object holds
( s in PreNorms ONE iff s = 1 )
proof
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 ;
hereby :: thesis: ( s = 1 implies s in PreNorms ONE )
assume s in PreNorms ONE ; :: thesis: s = 1
then consider t being Element of X such that
A5: s = |.(ONE . t).| ;
thus s = 1 by ; :: thesis: verum
end;
assume s = 1 ; :: thesis: s in PreNorms ONE
hence s in PreNorms ONE by ; :: thesis: verum
end;
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 :: thesis: for a being Complex
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 ;
now :: thesis: for x being Element of X holds h3 . x = (f1 . x) * (h1 . x)
let x be Element of X; :: thesis: h3 . x = (f1 . x) * (h1 . x)
h3 . x = a * (h2 . x) by ;
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 ; :: thesis: verum
end;
hence a * (f * g) = f * (a * g) by A8, A12, A10, Th24; :: thesis: verum
end;
A13: now :: thesis: for f, g being Element of B holds ||.(f * g).|| <= *
let f, g be Element of B; :: thesis: ||.(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 ;
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 ;
now :: thesis: for s being Real st s in PreNorms h1 holds
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 ;
|.(f1 . t).| in PreNorms f1 ;
then A24: |.(f1 . t).| <= upper_bound (PreNorms f1) by ;
then A25: (upper_bound (PreNorms f1)) * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by ;
A26: |.(f1 . t).| * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * |.(g1 . t).| by ;
|.(h1 . t).| = |.((f1 . t) * (g1 . t)).| by ;
then |.(h1 . t).| = |.(f1 . t).| * |.(g1 . t).| by COMPLEX1:65;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by ; :: thesis: 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 ;
||.f.|| = upper_bound (PreNorms f1) by ;
hence ||.(f * g).|| <= * by A19, A20, A28, A27, Th13; :: thesis: verum
end;
A29: now :: thesis: for f, g, h being Element of B holds (g + h) * f = (g * f) + (h * f)
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 ;
now :: thesis: for x being Element of X holds F1 . x = (gf1 . x) + (hf1 . x)
let x be Element of X; :: thesis: F1 . x = (gf1 . x) + (hf1 . x)
F1 . x = (gPh1 . x) * (f1 . x) by ;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by ;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by ;
hence F1 . x = (gf1 . x) + (hf1 . x) by ; :: thesis: verum
end;
hence (g + h) * f = (g * f) + (h * f) by ; :: thesis: 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 ;
A39: B is Banach_Algebra-like_2 by ;
A40: B is Banach_Algebra-like_3 by ;
B is left-distributive by A29;
hence C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra by A37, A38, A39, A40; :: thesis: verum