:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;

attr V1 is having-inverse means :: C0SP1:def 1
for v being Element of V st v in V1 holds
- v in V1;

end;

:: deftheorem defines having-inverse C0SP1:def 1 :
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is having-inverse iff for v being Element of V st v in V1 holds
- v in V1 );

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;

attr V1 is additively-closed means :: C0SP1:def 2
( V1 is add-closed & V1 is having-inverse );

end;

:: deftheorem defines additively-closed C0SP1:def 2 :
for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );

Lm1: for V being non empty addLoopStr holds [#] V is add-closed

proof end;

registration

let V be non empty addLoopStr ;

cluster [#] V -> add-closed having-inverse ;

correctness
coherence
( [#] V is add-closed & [#] V is having-inverse );
by Lm1;

end;

registration

let V be non empty doubleLoopStr ;

cluster additively-closed -> add-closed having-inverse for Element of bool the carrier of V;

coherence
for b₁ being Subset of V st b₁ is additively-closed holds
( b₁ is add-closed & b₁ is having-inverse ) ;

cluster add-closed having-inverse -> additively-closed for Element of bool the carrier of V;

coherence
for b₁ being Subset of V st b₁ is add-closed & b₁ is having-inverse holds
b₁ is additively-closed ;

end;

registration

let V be non empty addLoopStr ;

cluster non empty add-closed having-inverse for Element of bool the carrier of V;

correctness
existence
ex b₁ being Subset of V st
( b₁ is add-closed & b₁ is having-inverse & not b₁ is empty );

proof end;

end;

definition

let V be Ring;

mode Subring of V -> Ring means :Def3: :: C0SP1:def 3
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & 1. it = 1. V & 0. it = 0. V );

existence
ex b₁ being Ring st
( the carrier of b₁ c= the carrier of V & the addF of b₁ = the addF of V || the carrier of b₁ & the multF of b₁ = the multF of V || the carrier of b₁ & 1. b₁ = 1. V & 0. b₁ = 0. V )

proof end;

end;

:: deftheorem Def3 defines Subring C0SP1:def 3 :
for V, b₂ being Ring holds
( b₂ is Subring of V iff ( the carrier of b₂ c= the carrier of V & the addF of b₂ = the addF of V || the carrier of b₂ & the multF of b₂ = the multF of V || the carrier of b₂ & 1. b₂ = 1. V & 0. b₂ = 0. V ) );

theorem Th1: :: C0SP1:1

for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V

proof end;

registration

let V be Ring;

cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed V105() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative for Subring of V;

existence
ex b₁ being Subring of V st b₁ is strict

proof end;

end;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;

attr V1 is multiplicatively-closed means :: C0SP1:def 4
( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) );

end;

:: deftheorem defines multiplicatively-closed C0SP1:def 4 :
for V being non empty multLoopStr_0
for V1 being Subset of V holds
( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) ) );

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & not V1 is empty ) ;

func Add_ (V1,V) -> BinOp of V1 equals :Def5: :: C0SP1:def 5
the addF of V || V1;

correctness
coherence
the addF of V || V1 is BinOp of V1;

proof end;

end;

:: deftheorem Def5 defines Add_ C0SP1:def 5 :
for V being non empty addLoopStr
for V1 being Subset of V st V1 is add-closed & not V1 is empty holds
Add_ (V1,V) = the addF of V || V1;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

func mult_ (V1,V) -> BinOp of V1 equals :Def6: :: C0SP1:def 6
the multF of V || V1;

correctness
coherence
the multF of V || V1 is BinOp of V1;

proof end;

end;

:: deftheorem Def6 defines mult_ C0SP1:def 6 :
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
mult_ (V1,V) = the multF of V || V1;

definition

let V be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) ;

func Zero_ (V1,V) -> Element of V1 equals :Def7: :: C0SP1:def 7
0. V;

correctness
coherence
0. V is Element of V1;

proof end;

end;

:: deftheorem Def7 defines Zero_ C0SP1:def 7 :
for V being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds
Zero_ (V1,V) = 0. V;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;

func One_ (V1,V) -> Element of V1 equals :Def8: :: C0SP1:def 8
1. V;

correctness
coherence
1. V is Element of V1;
by A1;

end;

:: deftheorem Def8 defines One_ C0SP1:def 8 :
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
One_ (V1,V) = 1. V;

theorem :: C0SP1:2

for V being Ring
for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds
doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring

proof end;

definition

let V be Algebra;

mode Subalgebra of V -> Algebra means :Def9: :: C0SP1:def 9
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );

existence
ex b₁ being Algebra st
( the carrier of b₁ c= the carrier of V & the addF of b₁ = the addF of V || the carrier of b₁ & the multF of b₁ = the multF of V || the carrier of b₁ & the Mult of b₁ = the Mult of V | [:REAL, the carrier of b₁:] & 1. b₁ = 1. V & 0. b₁ = 0. V )

proof end;

end;

:: deftheorem Def9 defines Subalgebra C0SP1:def 9 :
for V, b₂ being Algebra holds
( b₂ is Subalgebra of V iff ( the carrier of b₂ c= the carrier of V & the addF of b₂ = the addF of V || the carrier of b₂ & the multF of b₂ = the multF of V || the carrier of b₂ & the Mult of b₂ = the Mult of V | [:REAL, the carrier of b₂:] & 1. b₂ = 1. V & 0. b₂ = 0. V ) );

theorem Th3: :: C0SP1:3

for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V

proof end;

registration

let V be Algebra;

cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V105() strict vector-associative right-distributive right_unital well-unital left_unital unital associative commutative for Subalgebra of V;

existence
ex b₁ being Subalgebra of V st b₁ is strict

proof end;

end;

definition

let V be Algebra;
let V1 be Subset of V;

attr V1 is additively-linearly-closed means :: C0SP1:def 10
( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) );

end;

:: deftheorem defines additively-linearly-closed C0SP1:def 10 :
for V being Algebra
for V1 being Subset of V holds
( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) ) );

registration

let V be Algebra;

cluster additively-linearly-closed -> additively-closed for Element of bool the carrier of V;

coherence
for b₁ being Subset of V st b₁ is additively-linearly-closed holds
b₁ is additively-closed ;

end;

definition

let V be Algebra;
let V1 be Subset of V;
assume A1: ( V1 is additively-linearly-closed & not V1 is empty ) ;

func Mult_ (V1,V) -> Function of [:REAL,V1:],V1 equals :Def11: :: C0SP1:def 11
the Mult of V | [:REAL,V1:];

correctness
coherence
the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1;

proof end;

end;

:: deftheorem Def11 defines Mult_ C0SP1:def 11 :
for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & not V1 is empty holds
Mult_ (V1,V) = the Mult of V | [:REAL,V1:];

definition

let V be non empty RLSStruct ;

attr V is scalar-mult-cancelable means :: C0SP1:def 12
for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );

end;

:: deftheorem defines scalar-mult-cancelable C0SP1:def 12 :
for V being non empty RLSStruct holds
( V is scalar-mult-cancelable iff for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );

theorem Th4: :: C0SP1:4

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr
for a being Real holds a * (0. V) = 0. V

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem :: C0SP1:5

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace

proof end;

Lm2: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace
by RLVECT_1:def 8;

theorem Th6: :: C0SP1:6

for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds
AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V

proof end;

registration

let X be non empty set ;

cluster RAlgebra X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative right-distributive right_unital associative commutative ;

correctness
coherence
( RAlgebra X is Abelian & RAlgebra X is add-associative & RAlgebra X is right_zeroed & RAlgebra X is right_complementable & RAlgebra X is commutative & RAlgebra X is associative & RAlgebra X is right_unital & RAlgebra X is right-distributive & RAlgebra X is vector-distributive & RAlgebra X is scalar-distributive & RAlgebra X is scalar-associative & RAlgebra X is vector-associative );
;

end;

theorem Th7: :: C0SP1:7

for X being non empty set holds RAlgebra X is RealLinearSpace

proof end;

theorem Th8: :: C0SP1:8

for V being Algebra
for V1 being Subalgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

definition

let X be non empty set ;

func BoundedFunctions X -> non empty Subset of (RAlgebra X) equals :: C0SP1:def 13
{ f where f is Function of X,REAL : f | X is bounded } ;

correctness
coherence
{ f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X);

proof end;

end;

:: deftheorem defines BoundedFunctions C0SP1:def 13 :
for X being non empty set holds BoundedFunctions X = { f where f is Function of X,REAL : f | X is bounded } ;

theorem Th9: :: C0SP1:9

for X being non empty set holds
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )

proof end;

registration

let X be non empty set ;

cluster BoundedFunctions X -> non empty multiplicatively-closed additively-linearly-closed ;

coherence
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed ) by Th9;

end;

definition

let X be non empty set ;

func R_Algebra_of_BoundedFunctions X -> Algebra equals :: C0SP1:def 14
AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

coherence
AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #) is Algebra by Th6;

end;

:: deftheorem defines R_Algebra_of_BoundedFunctions C0SP1:def 14 :
for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);

theorem :: C0SP1:10

for X being non empty set holds R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;

theorem :: C0SP1:11

for X being non empty set holds R_Algebra_of_BoundedFunctions X is RealLinearSpace

proof end;

theorem Th12: :: C0SP1:12

for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th13: :: C0SP1:13

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

proof end;

theorem Th14: :: C0SP1:14

for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,REAL st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th15: :: C0SP1:15

for X being non empty set holds 0. (R_Algebra_of_BoundedFunctions X) = X --> 0

proof end;

theorem Th16: :: C0SP1:16

for X being non empty set holds 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1

proof end;

definition

let X be non empty set ;
let F be object ;
assume A1: F in BoundedFunctions X ;

func modetrans (F,X) -> Function of X,REAL means :Def15: :: C0SP1:def 15
( it = F & it | X is bounded );

correctness
existence
ex b₁ being Function of X,REAL st
( b₁ = F & b₁ | X is bounded );
uniqueness
for b₁, b₂ being Function of X,REAL st b₁ = F & b₁ | X is bounded & b₂ = F & b₂ | X is bounded holds
b₁ = b₂;
by A1;

end;

:: deftheorem Def15 defines modetrans C0SP1:def 15 :
for X being non empty set
for F being object st F in BoundedFunctions X holds
for b₃ being Function of X,REAL holds
( b₃ = modetrans (F,X) iff ( b₃ = F & b₃ | X is bounded ) );

definition

let X be non empty set ;
let f be Function of X,REAL;

func PreNorms f -> non empty Subset of REAL equals :: C0SP1:def 16
{ |.(f . x).| where x is Element of X : verum } ;

coherence
{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL

proof end;

end;

:: deftheorem defines PreNorms C0SP1:def 16 :
for X being non empty set
for f being Function of X,REAL holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;

theorem Th17: :: C0SP1:17

for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above

proof end;

theorem :: C0SP1:18

for X being non empty set
for f being Function of X,REAL holds
( f | X is bounded iff PreNorms f is bounded_above )

proof end;

definition

let X be non empty set ;

func BoundedFunctionsNorm X -> Function of (BoundedFunctions X),REAL means :Def17: :: C0SP1:def 17
for x being object st x in BoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));

existence
ex b₁ being Function of (BoundedFunctions X),REAL st
for x being object st x in BoundedFunctions X holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X)))

proof end;

uniqueness
for b₁, b₂ being Function of (BoundedFunctions X),REAL st ( for x being object st x in BoundedFunctions X holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being object st x in BoundedFunctions X holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def 17 :
for X being non empty set
for b₂ being Function of (BoundedFunctions X),REAL holds
( b₂ = BoundedFunctionsNorm X iff for x being object st x in BoundedFunctions X holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X))) );

theorem Th19: :: C0SP1:19

for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
modetrans (f,X) = f

proof end;

theorem Th20: :: C0SP1:20

for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be non empty set ;

func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals :: C0SP1:def 18
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

correctness
coherence
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;
;

end;

:: deftheorem defines R_Normed_Algebra_of_BoundedFunctions C0SP1:def 18 :
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);

registration

let X be non empty set ;

cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty ;

correctness
coherence
not R_Normed_Algebra_of_BoundedFunctions X is empty ;
;

end;

Lm3: now :: thesis: for X being non empty set
for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds
( x * e = x & e * x = x )

let X be non empty set ; :: thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_BoundedFunctions X;
let x, e be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( e = One_ ((BoundedFunctions X),(RAlgebra X)) implies ( x * e = x & e * x = x ) )
set X1 = BoundedFunctions X;
reconsider f = x as Element of BoundedFunctions X ;
assume A1: e = One_ ((BoundedFunctions X),(RAlgebra X)) ; :: thesis: ( x * e = x & e * x = x )
then x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (f,(1_ (RAlgebra X))) by Def8;
then A2: x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (f,(1_ (RAlgebra X))) by Def6;
e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . ((1_ (RAlgebra X)),f) by A1, Def8;
then A3: e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . ((1_ (RAlgebra X)),f) by Def6;
A4: 1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by Th16;
then [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] by ZFMISC_1:87;
then x * e = f * (1_ (RAlgebra X)) by A2, FUNCT_1:49;
hence x * e = x ; :: thesis: e * x = x
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] by A4, ZFMISC_1:87;
then e * x = (1_ (RAlgebra X)) * f by A3, FUNCT_1:49;
hence e * x = x ; :: thesis: verum

end;

registration

let X be non empty set ;

cluster R_Normed_Algebra_of_BoundedFunctions X -> unital ;

correctness
coherence
R_Normed_Algebra_of_BoundedFunctions X is unital ;

proof end;

end;

theorem Th21: :: C0SP1:21

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 OneF of W, the ZeroF of W #) = V holds
W is Algebra

proof end;

theorem Th22: :: C0SP1:22

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Algebra

proof end;

theorem Th23: :: C0SP1:23

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F

proof end;

theorem Th24: :: C0SP1:24

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace

proof end;

theorem Th25: :: C0SP1:25

for X being non empty set holds X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)

proof end;

theorem Th26: :: C0SP1:26

for X being non empty set
for x being Element of X
for f being Function of X,REAL
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||

proof end;

theorem :: C0SP1:27

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

proof end;

theorem Th28: :: C0SP1:28

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||

proof end;

theorem Th29: :: C0SP1:29

for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th30: :: C0SP1:30

for X being non empty set
for a being Real
for f, g being Function of X,REAL
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th31: :: C0SP1:31

for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th32: :: C0SP1:32

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

proof end;

theorem Th33: :: C0SP1:33

for X being non empty set holds
( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )

proof end;

registration

let X be non empty set ;

cluster R_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence
( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is vector-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-associative & R_Normed_Algebra_of_BoundedFunctions X is scalar-unital & R_Normed_Algebra_of_BoundedFunctions X is Abelian & R_Normed_Algebra_of_BoundedFunctions X is add-associative & R_Normed_Algebra_of_BoundedFunctions X is right_zeroed & R_Normed_Algebra_of_BoundedFunctions X is right_complementable ) by Th24, Th33;

end;

theorem Th34: :: C0SP1:34

for X being non empty set
for f, g, h being Function of X,REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

proof end;

theorem Th35: :: C0SP1:35

for X being non empty set
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof end;

theorem Th36: :: C0SP1:36

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace

proof end;

registration

let X be non empty set ;

cluster R_Normed_Algebra_of_BoundedFunctions X -> complete ;

coherence
R_Normed_Algebra_of_BoundedFunctions X is complete by Th36;

end;

registration

let X be non empty set ;

cluster R_Normed_Algebra_of_BoundedFunctions X -> left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 ;

coherence
( R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_1 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )

proof end;

end;

theorem :: C0SP1:37

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra by Th22;