:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Rdef210b defines having-inverse C0SP1:def 1 :
:: deftheorem Rdef210 defines additively-closed C0SP1:def 2 :
Cor1:
for V being non empty addLoopStr holds [#] V is add-closed
Cor2:
for V being non empty addLoopStr holds [#] V is having-inverse
:: deftheorem DefSubRing defines Subring C0SP1:def 3 :
theorem Th01: :: C0SP1:1
:: deftheorem Rdef200 defines multiplicatively-closed C0SP1:def 4 :
:: deftheorem Rdef211 defines Add_ C0SP1:def 5 :
:: deftheorem Rdef220 defines mult_ C0SP1:def 6 :
:: deftheorem Rdef213 defines Zero_ C0SP1:def 7 :
:: deftheorem Rdef214 defines One_ C0SP1:def 8 :
theorem :: C0SP1:2
:: deftheorem DefSubAlg defines Subalgebra C0SP1:def 9 :
theorem Th02: :: 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
:: deftheorem def210 defines additively-linearly-closed C0SP1:def 10 :
:: deftheorem def212 defines Mult_ C0SP1:def 11 :
:: deftheorem DefSMC defines scalar-mult-cancelable C0SP1:def 12 :
theorem RLVECT123: :: C0SP1:4
theorem :: C0SP1:5
LmAlgebra:
for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace
theorem Th03: :: 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
theorem LmAlgebra2: :: C0SP1:7
theorem RLSUB121: :: C0SP1:8
:: deftheorem defines BoundedFunctions C0SP1:def 13 :
theorem ThB7: :: C0SP1:9
theorem :: C0SP1:10
for
X being non
empty set holds
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
Subalgebra of
RAlgebra X by Th03;
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 Th03;
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:11
theorem ThB10: :: C0SP1:12
theorem ThB11: :: C0SP1:13
theorem ThB12: :: C0SP1:14
theorem ThB12Zero: :: C0SP1:15
theorem ThB12One: :: C0SP1:16
:: deftheorem DefB7 defines modetrans C0SP1:def 15 :
:: deftheorem defines PreNorms C0SP1:def 16 :
theorem ThB13: :: C0SP1:17
theorem :: C0SP1:18
theorem ThB15: :: C0SP1:19
:: deftheorem DefB9 defines BoundedFunctionsNorm C0SP1:def 17 :
theorem ThB16: :: C0SP1:20
theorem ThB17: :: C0SP1:21
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) #);
UNITAL:
now
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 ) )assume A1:
e = One_ (BoundedFunctions X),
(RAlgebra X)
;
:: thesis: ( x * e = x & e * x = x )set X1 =
BoundedFunctions X;
reconsider f =
x as
Element of
BoundedFunctions X ;
1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X)
by ThB12One;
then P5:
(
[f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] &
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] )
by ZFMISC_1:106;
x * e = (mult_ (BoundedFunctions X),(RAlgebra X)) . f,
(1_ (RAlgebra X))
by A1, Rdef214;
then
x * e = (the multF of (RAlgebra X) || (BoundedFunctions X)) . f,
(1_ (RAlgebra X))
by Rdef220;
then
x * e = f * (1_ (RAlgebra X))
by P5, FUNCT_1:72;
hence
x * e = x
by FUNCSDOM:49;
:: thesis: e * x = x
e * x = (mult_ (BoundedFunctions X),(RAlgebra X)) . (1_ (RAlgebra X)),
f
by A1, Rdef214;
then
e * x = (the multF of (RAlgebra X) || (BoundedFunctions X)) . (1_ (RAlgebra X)),
f
by Rdef220;
then
e * x = (1_ (RAlgebra X)) * f
by P5, FUNCT_1:72;
hence
e * x = x
by FUNCSDOM:49;
:: thesis: verum
end;
theorem RSSPACE34: :: C0SP1:22
theorem LmAlgebra4: :: C0SP1:23
theorem FUNCSDOM23: :: C0SP1:24
theorem LmAlgebra5: :: C0SP1:25
theorem ThB18: :: C0SP1:26
theorem ThB19: :: C0SP1:27
theorem :: C0SP1:28
theorem ThB21: :: C0SP1:29
theorem ThB22: :: C0SP1:30
theorem ThB23: :: C0SP1:31
theorem ThB23a: :: C0SP1:32
theorem ThB24: :: C0SP1:33
theorem ThB25: :: C0SP1:34
theorem ThB27: :: C0SP1:35
theorem ThB28: :: C0SP1:36
theorem ThB29: :: C0SP1:37
theorem :: C0SP1:38