:: 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 Def1 defines having-inverse C0SP1:def 1 :
:: deftheorem Def2 defines additively-closed C0SP1:def 2 :
Lm1:
for V being non empty addLoopStr holds [#] V is add-closed
Lm2:
for V being non empty addLoopStr holds [#] V is having-inverse
:: deftheorem Def3 defines Subring C0SP1:def 3 :
theorem Th1: :: C0SP1:1
:: deftheorem Def4 defines multiplicatively-closed C0SP1:def 4 :
:: deftheorem Def5 defines Add_ C0SP1:def 5 :
:: deftheorem Def6 defines mult_ C0SP1:def 6 :
:: deftheorem Def7 defines Zero_ C0SP1:def 7 :
:: deftheorem Def8 defines One_ C0SP1:def 8 :
theorem :: C0SP1:2
:: deftheorem Def9 defines Subalgebra C0SP1:def 9 :
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
:: deftheorem Def10 defines additively-linearly-closed C0SP1:def 10 :
:: deftheorem Def11 defines Mult_ C0SP1:def 11 :
:: deftheorem Def12 defines scalar-mult-cancelable C0SP1:def 12 :
theorem Th4: :: C0SP1:4
theorem :: C0SP1:5
Lm3:
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 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
theorem Th7: :: C0SP1:7
theorem Th8: :: C0SP1:8
:: deftheorem defines BoundedFunctions C0SP1:def 13 :
theorem Th9: :: 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 Th6;
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:11
theorem Th12: :: C0SP1:12
theorem Th13: :: C0SP1:13
theorem Th14: :: C0SP1:14
theorem Th15: :: C0SP1:15
theorem Th16: :: C0SP1:16
:: deftheorem Def15 defines modetrans C0SP1:def 15 :
:: deftheorem defines PreNorms C0SP1:def 16 :
theorem Th17: :: C0SP1:17
theorem :: C0SP1:18
theorem Th19: :: C0SP1:19
:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def 17 :
theorem Th20: :: C0SP1:20
theorem Th21: :: 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) #);
Lm4:
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 ) )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:106;
then
x * e = f * (1_ (RAlgebra X))
by A2, FUNCT_1:72;
hence
x * e = x
by FUNCSDOM:49;
:: thesis: e * x = x
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):]
by A4, ZFMISC_1:106;
then
e * x = (1_ (RAlgebra X)) * f
by A3, FUNCT_1:72;
hence
e * x = x
by FUNCSDOM:49;
:: thesis: verum
end;
theorem Th22: :: C0SP1:22
theorem Th23: :: C0SP1:23
theorem Th24: :: C0SP1:24
theorem Th25: :: C0SP1:25
theorem Th26: :: C0SP1:26
theorem Th27: :: C0SP1:27
theorem :: C0SP1:28
theorem Th29: :: C0SP1:29
theorem Th30: :: C0SP1:30
theorem Th31: :: C0SP1:31
theorem Th32: :: C0SP1:32
theorem Th33: :: C0SP1:33
theorem Th34: :: C0SP1:34
theorem Th35: :: C0SP1:35
theorem Th36: :: C0SP1:36
theorem Th37: :: C0SP1:37
theorem :: C0SP1:38