:: Banach Algebra of Continuous Functionals
:: by Kanazashi Katuhiko , Noboru Endou and Yasunari Shidama
::
:: Received October 20, 2009
:: Copyright (c) 2009 Association of Mizar Users

begin

definition

let X be 1-sorted ;
let y be real number ;
func X --> y -> RealMap of X equals :: C0SP2:def 1
the carrier of X --> y;
coherence
the carrier of X --> y is RealMap of X

proof end;

end;

:: deftheorem defines --> C0SP2:def 1 :

for X being 1-sorted
for y being real number holds X --> y = the carrier of X --> y;

registration

let X be TopSpace;
let y be real number ;
cluster X --> y -> continuous ;
coherence
X --> y is continuous

proof end;

end;

theorem LMcont: :: C0SP2:1

for X being non empty TopSpace
for f being RealMap of X holds
( f is continuous iff for x being Point of
for V being Subset of st f . x in V & V is open holds
ex W being Subset of st
( x in W & W is open & f .: W c= V ) )

proof end;

LmAlgebra: for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st ( for v being VECTOR of holds 1 * v = v ) holds
V is RealLinearSpace

proof end;

definition

let X be non empty TopSpace;
func ContinuousFunctions X -> Subset of equals :: C0SP2:def 2
{ f where f is continuous RealMap of X : verum } ;
correctness
coherence
{ f where f is continuous RealMap of X : verum } is Subset of ;

proof end;

end;

:: deftheorem defines ContinuousFunctions C0SP2:def 2 :

for X being non empty TopSpace holds ContinuousFunctions X = { f where f is continuous RealMap of X : verum } ;

registration

let X be non empty TopSpace;
cluster ContinuousFunctions X -> non empty ;
coherence
not ContinuousFunctions X is empty

proof end;

end;

registration

let X be non empty TopSpace;
cluster ContinuousFunctions X -> multiplicatively-closed additively-linearly-closed ;
coherence
( ContinuousFunctions X is additively-linearly-closed & ContinuousFunctions X is multiplicatively-closed )

proof end;

end;

theorem :: C0SP2:2

for X being non empty TopSpace holds AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #) is Subalgebra of RAlgebra the carrier of X by C0SP1:6;

definition

let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals :: C0SP2:def 3
AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #);
coherence
AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #) is AlgebraStr ;

end;

:: deftheorem defines R_Algebra_of_ContinuousFunctions C0SP2:def 3 :

for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X = AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #);

registration

let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions X -> non empty strict ;
coherence
( R_Algebra_of_ContinuousFunctions X is strict & not R_Algebra_of_ContinuousFunctions X is empty ) ;

end;

registration

let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like associative commutative right-distributive right_unital Algebra-like ;
coherence
( R_Algebra_of_ContinuousFunctions X is Abelian & R_Algebra_of_ContinuousFunctions X is add-associative & R_Algebra_of_ContinuousFunctions X is right_zeroed & R_Algebra_of_ContinuousFunctions X is right_complementable & R_Algebra_of_ContinuousFunctions X is RealLinearSpace-like & R_Algebra_of_ContinuousFunctions X is commutative & R_Algebra_of_ContinuousFunctions X is associative & R_Algebra_of_ContinuousFunctions X is right_unital & R_Algebra_of_ContinuousFunctions X is right-distributive & R_Algebra_of_ContinuousFunctions X is Algebra-like )

proof end;

end;

theorem ThB10: :: C0SP2:3

for X being non empty TopSpace
for F, G, H being VECTOR of
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )

proof end;

theorem ThB11: :: C0SP2:4

for X being non empty TopSpace
for F, G being VECTOR of
for f, g being RealMap of X
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of holds g . x = a * (f . x) )

proof end;

theorem ThB12: :: C0SP2:5

for X being non empty TopSpace
for F, G, H being VECTOR of
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )

proof end;

theorem ThB12Zero: :: C0SP2:6

for X being non empty TopSpace holds 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0

proof end;

theorem ThB12One: :: C0SP2:7

for X being non empty TopSpace holds 1_ (R_Algebra_of_ContinuousFunctions X) = X --> 1

proof end;

theorem subalgebra: :: C0SP2:8

for A being Algebra
for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is Subalgebra of A2

proof end;

LMX01: for X being non empty compact TopSpace
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X

proof end;

theorem :: C0SP2:9

for X being non empty compact TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X

proof end;

definition

let X be non empty compact TopSpace;
func ContinuousFunctionsNorm X -> Function of ContinuousFunctions X, REAL equals :: C0SP2:def 4
(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);
correctness
coherence
(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of ContinuousFunctions X, REAL ;

proof end;

end;

:: deftheorem defines ContinuousFunctionsNorm C0SP2:def 4 :

for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);

definition

let X be non empty compact TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals :: C0SP2:def 5
Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(ContinuousFunctionsNorm X) #);
correctness
coherence
Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(ContinuousFunctionsNorm X) #) is Normed_AlgebraStr ;
;

end;

:: deftheorem defines R_Normed_Algebra_of_ContinuousFunctions C0SP2:def 5 :

for X being non empty compact TopSpace holds R_Normed_Algebra_of_ContinuousFunctions X = Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(ContinuousFunctionsNorm X) #);

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> non empty strict ;
correctness
coherence
( R_Normed_Algebra_of_ContinuousFunctions X is strict & not R_Normed_Algebra_of_ContinuousFunctions X is empty );
;

end;

UNITAL: now

let X be non empty compact TopSpace; :: thesis: for x, e being Element of st e = One_ (ContinuousFunctions X),(RAlgebra the carrier of X) holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_ContinuousFunctions X;
let x, e be Element of ; :: thesis: ( e = One_ (ContinuousFunctions X),(RAlgebra the carrier of X) implies ( x * e = x & e * x = x ) )
assume A1: e = One_ (ContinuousFunctions X),(RAlgebra the carrier of X) ; :: thesis: ( x * e = x & e * x = x )
set X1 = ContinuousFunctions X;
reconsider f = x as Element of ContinuousFunctions X ;
1_ (RAlgebra the carrier of X) = X --> 1
.= 1_ (R_Algebra_of_ContinuousFunctions X) by ThB12One ;
then A2: ( [f,(1_ (RAlgebra the carrier of X))] in [:(ContinuousFunctions X),(ContinuousFunctions X):] & [(1_ (RAlgebra the carrier of X)),f] in [:(ContinuousFunctions X),(ContinuousFunctions X):] ) by ZFMISC_1:106;
x * e = (mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . f,(1_ (RAlgebra the carrier of X)) by A1, C0SP1:def 8;
then x * e = (the multF of (RAlgebra the carrier of X) || (ContinuousFunctions X)) . f,(1_ (RAlgebra the carrier of X)) by C0SP1:def 6;
then x * e = f * (1_ (RAlgebra the carrier of X)) by A2, FUNCT_1:72;
hence x * e = x by FUNCSDOM:49; :: thesis: e * x = x
e * x = (mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . (1_ (RAlgebra the carrier of X)),f by A1, C0SP1:def 8;
then e * x = (the multF of (RAlgebra the carrier of X) || (ContinuousFunctions X)) . (1_ (RAlgebra the carrier of X)),f by C0SP1:def 6;
then e * x = (1_ (RAlgebra the carrier of X)) * f by A2, FUNCT_1:72;
hence e * x = x by FUNCSDOM:49; :: thesis: verum

end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> unital ;
correctness
coherence
R_Normed_Algebra_of_ContinuousFunctions X is unital ;

proof end;

end;

theorem RSSPACE34: :: C0SP2:10

for W being Normed_AlgebraStr
for V being Algebra st AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the U3 of W,the U2 of W #) = V holds
W is Algebra

proof end;

LMX02: for X being non empty compact TopSpace
for x being Point of
for y being Point of st x = y holds
||.x.|| = ||.y.||

proof end;

LMX03: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2

proof end;

LMX04: for X being non empty compact TopSpace
for a being Real
for x being Point of
for y being Point of st x = y holds
a * x = a * y

proof end;

LMX05: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2

proof end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital Algebra-like ;
coherence
( R_Normed_Algebra_of_ContinuousFunctions X is Abelian & R_Normed_Algebra_of_ContinuousFunctions X is add-associative & R_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & R_Normed_Algebra_of_ContinuousFunctions X is right_complementable & R_Normed_Algebra_of_ContinuousFunctions X is commutative & R_Normed_Algebra_of_ContinuousFunctions X is associative & R_Normed_Algebra_of_ContinuousFunctions X is right_unital & R_Normed_Algebra_of_ContinuousFunctions X is right-distributive & R_Normed_Algebra_of_ContinuousFunctions X is Algebra-like )

proof end;

end;

theorem FUNCSDOM23: :: C0SP2:11

for X being non empty compact TopSpace
for F being Point of holds (Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . 1,F = F

proof end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> RealLinearSpace-like ;
coherence
R_Normed_Algebra_of_ContinuousFunctions X is RealLinearSpace-like

proof end;

end;

theorem ThB18: :: C0SP2:12

for X being non empty compact TopSpace holds X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X)

proof end;

LMX06: for X being non empty compact TopSpace holds 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)

proof end;

LMX07: for X being non empty compact TopSpace holds 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)

proof end;

theorem :: C0SP2:13

for X being non empty compact TopSpace
for F being Point of holds 0 <= ||.F.||

proof end;

theorem :: C0SP2:14

for X being non empty compact TopSpace
for F being Point of st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds
0 = ||.F.||

proof end;

theorem ThB22: :: C0SP2:15

for X being non empty compact TopSpace
for f, g, h being RealMap of X
for F, G, H being Point of st f = F & g = G & h = H holds
( H = F + G iff for x being Element of holds h . x = (f . x) + (g . x) )

proof end;

theorem :: C0SP2:16

for a being Real
for X being non empty compact TopSpace
for f, g being RealMap of X
for F, G being Point of st f = F & g = G holds
( G = a * F iff for x being Element of holds g . x = a * (f . x) )

proof end;

theorem :: C0SP2:17

for X being non empty compact TopSpace
for f, g, h being RealMap of X
for F, G, H being Point of st f = F & g = G & h = H holds
( H = F * G iff for x being Element of holds h . x = (f . x) * (g . x) )

proof end;

theorem ThB24: :: C0SP2:18

for a being Real
for X being non empty compact TopSpace
for F, G being Point of holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> RealNormSpace-like ;
coherence
R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like

proof end;

end;

LMX03a: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2

proof end;

theorem :: C0SP2:19

for X being non empty compact TopSpace
for f, g, h being RealMap of X
for F, G, H being Point of st f = F & g = G & h = H holds
( H = F - G iff for x being Element of holds h . x = (f . x) - (g . x) )

proof end;

theorem SUBSP1: :: C0SP2:20

for X being complete RealNormSpace
for Y being Subset of
for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds
( seq is convergent & lim seq in Y )

proof end;

theorem SUBSP2: :: C0SP2:21

for X being non empty compact TopSpace
for Y being Subset of st Y = ContinuousFunctions X holds
Y is closed

proof end;

theorem ThB28: :: C0SP2:22

for X being non empty compact TopSpace
for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent

proof end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> complete ;
coherence
R_Normed_Algebra_of_ContinuousFunctions X is complete

proof end;

end;

registration

let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like ;
coherence
R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like

proof end;

end;