:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3,
FUNCSDOM, STRUCT_0, TARSKI, REALSET1, MESFUNC1, SUPINF_2, BINOP_1,
FUNCT_1, ZFMISC_1, RELAT_1, RLVECT_1, VECTSP_1, LATTICES, RSSPACE,
GROUP_1, REAL_1, POLYALG1, CARD_1, RSSPACE4, XXREAL_2, FUNCOP_1, FUNCT_2,
VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, SEQ_4, ORDINAL2, LOPBAN_2,
PRE_TOPC, NORMSP_1, NAT_1, RSSPACE3, SEQ_2, SEQ_1, REWRITE1, C0SP1,
METRIC_1, RELAT_2, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, STRUCT_0, ALGSTR_0,
REAL_1, REALSET1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, RELSET_1,
PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, PARTFUN1, IDEAL_1,
RSSPACE3, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCOP_1, NORMSP_0, NORMSP_1,
LOPBAN_1, LOPBAN_2;
constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, BINOP_2, LOPBAN_2, SEQ_2,
IDEAL_1, SEQ_4, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0,
NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, XXREAL_0, RLVECT_1, VECTSP_1,
VECTSP_2, FUNCT_2, VALUED_0, VALUED_1, LOPBAN_2, FUNCOP_1, SEQ_4,
RFUNCT_1, RELSET_1, SEQ_1, SEQ_2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions ALGSTR_0, TARSKI, FUNCSDOM, RLVECT_1, VECTSP_1, GROUP_1, NORMSP_0,
XXREAL_2, LOPBAN_2;
equalities REALSET1, ALGSTR_0, XCMPLX_0, FUNCSDOM, RLVECT_1, STRUCT_0,
BINOP_1, VALUED_1, NORMSP_0;
expansions ALGSTR_0, NORMSP_0, LOPBAN_2;
theorems SEQ_4, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, ALGSTR_0, COMPLEX1,
ZFMISC_1, TARSKI, RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM,
NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1,
FUNCOP_1, VECTSP_1, GROUP_1, VALUED_1, RSSPACE2, IDEAL_1, RELSET_1,
NORMSP_0, ORDINAL1;
schemes SEQ_1, FUNCT_2;
begin :: Some properties of Rings
definition
let V be non empty addLoopStr;
let V1 be Subset of V;
attr V1 is having-inverse means
for v be Element of V st v in V1 holds -v in V1;
end;
definition
let V be non empty addLoopStr;
let V1 be Subset of V;
attr V1 is additively-closed means
V1 is add-closed having-inverse;
end;
Lm1: for V be non empty addLoopStr holds [#]V is add-closed
proof
let V be non empty addLoopStr;
for v,u be Element of V st v in [#]V & u in [#]V holds v + u in [#]V;
hence thesis by IDEAL_1:def 1;
end;
registration
let V be non empty addLoopStr;
cluster [#]V -> add-closed having-inverse;
correctness by Lm1;
end;
registration
let V be non empty doubleLoopStr;
cluster additively-closed -> add-closed having-inverse for Subset of V;
coherence;
cluster add-closed having-inverse -> additively-closed for Subset of V;
coherence;
end;
registration
let V be non empty addLoopStr;
cluster add-closed having-inverse non empty for Subset of V;
correctness
proof
take [#]V;
thus thesis;
end;
end;
definition
let V be Ring;
mode Subring of V -> Ring means
:Def3:
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
proof
take V;
thus thesis by RELSET_1:19;
end;
end;
reserve X for non empty set;
reserve x for Element of X;
reserve d1,d2 for Element of X;
reserve A for BinOp of X;
reserve M for Function of [:X,X:],X;
reserve V for Ring;
reserve V1 for Subset of V;
theorem Th1:
V1 = X & A = (the addF of V)||V1 & M = (the multF of V)||V1 & d1
= 1.V & d2 = 0.V & V1 is having-inverse implies doubleLoopStr (# X,A,M,d1,d2 #)
is Subring of V
proof
assume that
A1: V1 = X and
A2: A = (the addF of V)||V1 and
A3: M = (the multF of V)||V1 and
A4: d1 = 1.V and
A5: d2 = 0.V and
A6: for v be Element of V st v in V1 holds -v in V1;
reconsider W = doubleLoopStr(# X,A,M,d1,d2 #) as non empty doubleLoopStr;
A7: now
let a,x be Element of W;
a*x = (the multF of V).([a,x]) by A1,A3,FUNCT_1:49;
hence a*x = (the multF of V).(a,x);
end;
A8: now
let x,y be Element of W;
x + y = (the addF of V).([x,y]) by A1,A2,FUNCT_1:49;
hence x + y = (the addF of V).(x,y);
end;
A9: W is Abelian add-associative right_zeroed right_complementable
associative well-unital distributive
proof
set MV = the multF of V;
set Av = the addF of V;
hereby
let x,y be Element of W;
reconsider x1 = x, y1 = y as Element of V by A1,TARSKI:def 3;
x + y = x1 + y1 & y + x = y1 + x1 by A8;
hence x + y = y + x;
end;
hereby
let x,y,z be Element of W;
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1,TARSKI:def 3;
x + (y + z) = Av.(x1,y + z) by A8;
then
A10: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = Av.(x +y,z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A10,RLVECT_1:def 3;
end;
hereby
let x be Element of W;
reconsider y = x as Element of V by A1,TARSKI:def 3;
x + 0.W = y + 0.V by A5,A8;
hence x + 0.W = x;
end;
thus W is right_complementable
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1,TARSKI:def 3;
consider v be Element of V such that
A11: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A11,VECTSP_1:16;
then reconsider y = v as Element of W by A1,A6;
take y;
thus thesis by A5,A8,A11;
end;
hereby
let a,b,x be Element of W;
reconsider y=x, a1=a, b1=b as Element of V by A1,TARSKI:def 3;
a * (b * x) = MV.(a,b * x) by A7;
then
A12: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A12,GROUP_1:def 3;
end;
hereby
let x be Element of W;
reconsider y = x as Element of V by A1,TARSKI:def 3;
x*1.W = y * 1.V & 1.W * x = 1.V * y by A4,A7;
hence x*1.W = x & 1.W * x =x;
end;
hereby
let a,x,y be Element of W;
reconsider x1=x, y1=y, a1=a as Element of V by A1,TARSKI:def 3;
(x+y)*a = MV.(x+y,a) by A7;
then (x+y)*a = (x1+y1)*a1 by A8;
then (x+y)*a = x1*a1 + y1*a1 by VECTSP_1:def 7;
then (x+y)*a = Av.(MV.(x1,a1),y*a) by A7;
then
A13: (x+y)*a = Av.(x*a,y*a) by A7;
a*(x+y) = MV.(a,x+y) by A7;
then a*(x+y) = a1*(x1+y1) by A8;
then a*(x+y) = a1*x1 + a1*y1 by VECTSP_1:def 7;
then a*(x+y) = Av.(MV.(a,x1),a*y) by A7;
then a*(x+y) = Av.(a*x,a*y) by A7;
hence a*(x+y) = a*x + a*y & (x+y)*a = x*a + y*a by A8,A13;
end;
end;
0.W = 0.V & 1.W = 1.V by A4,A5;
hence thesis by A1,A2,A3,A9,Def3;
end;
registration
let V be Ring;
cluster strict for Subring of V;
existence
proof
set V1 = [#]V;
the addF of V = (the addF of V)||V1 & the multF of V = (the multF of V
)||V1 by RELSET_1:19;
then
doubleLoopStr (# the carrier of V, the addF of V, the multF of V, 1.V,
0.V #) is Subring of V by Th1;
hence thesis;
end;
end;
definition
let V be non empty multLoopStr_0;
let V1 be Subset of V;
attr V1 is multiplicatively-closed means
1.V in V1 & for v,u be Element of V st v in V1 & u in V1 holds v * u in V1;
end;
definition
let V be non empty addLoopStr, V1 be Subset of V such that
A1: V1 is add-closed non empty;
func Add_(V1,V) -> BinOp of V1 equals
:Def5:
(the addF of V)||V1;
correctness
proof
A2: dom(the addF of V) = [:the carrier of V,the carrier of V:] by FUNCT_2:def 1
;
A3: for z be object st z in [:V1,V1:] holds ((the addF of V)||V1).z in V1
proof
let z be object;
assume
A4: z in [:V1,V1:];
then consider r,x be object such that
A5: r in V1 & x in V1 and
A6: z=[r,x] by ZFMISC_1:def 2;
reconsider y=x,r1=r as Element of V by A5;
[r,x] in dom((the addF of V)||V1) by A2,A4,A6,RELAT_1:62,ZFMISC_1:96;
then ((the addF of V)||V1).z = r1+y by A6,FUNCT_1:47;
hence thesis by A1,A5,IDEAL_1:def 1;
end;
dom((the addF of V)||V1) =[:V1,V1:] by A2,RELAT_1:62,ZFMISC_1:96;
hence thesis by A3,FUNCT_2:3;
end;
end;
definition
let V be non empty multLoopStr_0, V1 be Subset of V such that
A1: V1 is multiplicatively-closed non empty;
func mult_(V1,V) -> BinOp of V1 equals
:Def6:
(the multF of V)||V1;
correctness
proof
A2: dom(the multF of V) = [:the carrier of V,the carrier of V:] by
FUNCT_2:def 1;
A3: for z be object st z in [:V1,V1:] holds ((the multF of V)||V1).z in V1
proof
let z be object;
assume
A4: z in [:V1,V1:];
then consider r,x be object such that
A5: r in V1 & x in V1 and
A6: z=[r,x] by ZFMISC_1:def 2;
reconsider y=x,r1=r as Element of V by A5;
[r,x] in dom((the multF of V)||V1) by A2,A4,A6,RELAT_1:62,ZFMISC_1:96;
then ((the multF of V)||V1).z = r1*y by A6,FUNCT_1:47;
hence thesis by A1,A5;
end;
dom((the multF of V)||V1) =[:V1,V1:] by A2,RELAT_1:62,ZFMISC_1:96;
hence thesis by A3,FUNCT_2:3;
end;
end;
definition
let V be add-associative right_zeroed right_complementable non empty
doubleLoopStr, V1 be Subset of V such that
A1: V1 is add-closed having-inverse non empty;
func Zero_(V1,V) -> Element of V1 equals
:Def7:
0.V;
correctness
proof
set x = the Element of V1;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
-x1 in V1 & x1 + -x1 = 0.V by A1,RLVECT_1:def 10;
hence thesis by A1,IDEAL_1:def 1;
end;
end;
definition
let V be non empty multLoopStr_0, V1 be Subset of V such that
A1: V1 is multiplicatively-closed non empty;
func One_(V1,V) -> Element of V1 equals
:Def8:
1.V;
correctness by A1;
end;
theorem
V1 is additively-closed multiplicatively-closed non empty implies
doubleLoopStr(# V1,Add_(V1,V),mult_(V1,V),One_(V1,V),Zero_(V1,V) #) is Ring
proof
assume
A1: V1 is additively-closed multiplicatively-closed non empty;
then
A2: One_(V1,V) =1_V & mult_(V1,V) = (the multF of V) || V1 by Def6,Def8;
Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 by A1,Def5,Def7;
hence thesis by A1,A2,Th1;
end;
begin :: Some properties of Algebras
reserve V for Algebra;
reserve V1 for Subset of V;
reserve MR for Function of [:REAL,X:],X;
reserve a for Real;
definition
let V be Algebra;
mode Subalgebra of V -> Algebra means
:Def9:
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
proof
take V;
thus the carrier of V c= the carrier of V & the addF of V = (the addF of V
)||the carrier of V & the multF of V = (the multF of V)||the carrier of V & the
Mult of V = (the Mult of V) | [:REAL,the carrier of V:] & 1.V = 1.V & 0.V = 0.V
by RELSET_1:19;
end;
end;
theorem Th3:
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
implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
proof
assume that
A1: V1 = X and
A2: d1 = 0.V and
A3: d2 = 1.V and
A4: A = (the addF of V)||V1 and
A5: M = (the multF of V)||V1 and
A6: MR = (the Mult of V) | [:REAL,V1:] and
A7: for v be Element of V st v in V1 holds -v in V1;
reconsider W = AlgebraStr(# X,M,A,MR,d2,d1 #) as non empty AlgebraStr;
A8: now
let x,y be Element of W;
x + y = (the addF of V).[x,y] by A1,A4,FUNCT_1:49;
hence x + y = (the addF of V).(x,y);
end;
A9: now
let a,x be VECTOR of W;
a * x = (the multF of V).([a,x]) by A1,A5,FUNCT_1:49;
hence a * x = (the multF of V).(a,x);
end;
A10: now
let a;
let x be VECTOR of W;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
aa * x = (the Mult of V).([aa,x]) by A1,A6,FUNCT_1:49;
hence a * x = (the Mult of V).(a,x);
end;
A11: W is Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive vector-distributive
scalar-distributive scalar-associative vector-associative
proof
set Mv = the multF of V;
set Av = the addF of V;
hereby
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
x + y = x1 + y1 & y + x = y1 + x1 by A8;
hence x + y = y + x;
end;
hereby
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1,TARSKI:def 3;
x + (y + z) = Av.(x1,y + z) by A8;
then
A12: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = Av.(x + y,z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A12,RLVECT_1:def 3;
end;
hereby
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
thus x + 0.W = y + 0.V by A2,A8
.= x;
end;
thus W is right_complementable
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1,TARSKI:def 3;
consider v be Element of V such that
A13: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A13,VECTSP_1:16;
then reconsider y = v as Element of W by A1,A7;
take y;
thus thesis by A2,A8,A13;
end;
hereby
let v,w being Element of W;
reconsider v1 = v, w1=w as Element of V by A1,TARSKI:def 3;
v * w = v1 * w1 & w * v = w1 * v1 by A9;
hence v * w = w * v;
end;
hereby
let a,b,x be Element of W;
reconsider y=x, a1=a, b1=b as Element of V by A1,TARSKI:def 3;
a * (b * x) = Mv.(a,b * x) by A9;
then
A14: a * (b * x) = a1 * (b1 * y) by A9;
a * b = a1 * b1 by A9;
then (a * b) * x = (a1 * b1) * y by A9;
hence (a * b) * x = a * (b * x) by A14,GROUP_1:def 3;
end;
hereby
let v being Element of W;
reconsider v1 = v as Element of V by A1,TARSKI:def 3;
v * 1.W =v1*1.V by A3,A9;
hence v * 1.W = v;
end;
hereby
let x,y,z being Element of W;
reconsider x1=x, y1=y, z1=z as Element of V by A1,TARSKI:def 3;
y+z = y1+z1 by A8;
then x*(y+z) = x1*(y1+z1) by A9;
then
A15: x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 2;
x*y = x1*y1 & x*z = x1*z1 by A9;
hence x*(y+z) = x*y + x*z by A8,A15;
end;
thus W is vector-distributive
proof
let a be Real;
let x,y being Element of W;
reconsider x1=x, y1=y as Element of V by A1,TARSKI:def 3;
reconsider aa=a as Real;
A16: aa*x = aa*x1 by A10;
x+y = x1+y1 by A8;
then aa*(x+y) =aa*(x1+y1) by A10;
then
A17: a*(x+y) =a*x1 + a*y1 by RLVECT_1:def 5;
aa*y = aa*y1 by A10;
hence a*(x+y) = a*x + a*y by A8,A16,A17;
end;
thus W is scalar-distributive
proof
let a,b be Real;
reconsider aa=a, bb=b as Real;
let x being Element of W;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
A18: aa*x = aa*x1 by A10;
A19: bb*x = bb*x1 by A10;
(aa+bb)*x = (a+b)*x1 by A10;
then (a+b)*x = a*x1 + b*x1 by RLVECT_1:def 6;
hence (a+b)*x =a*x + b*x by A8,A18,A19;
end;
thus W is scalar-associative
proof
let a,b be Real;
let x being Element of W;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
reconsider aa=a, bb=b as Real;
A20: bb*x = bb*x1 by A10;
(aa*bb)*x = (a*b)*x1 by A10;
then (aa*bb)*x = a*(bb*x1) by RLVECT_1:def 7;
hence (a*b)*x = a*(b*x) by A10,A20;
end;
thus W is vector-associative
proof
let x,y being Element of W;
reconsider x1=x, y1=y as Element of V by A1,TARSKI:def 3;
let a be Real;
A21: a*x = a*x1 by A10;
x*y = x1*y1 by A9;
then a*(x*y) =a*(x1*y1) by A10;
then a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 9;
hence a*(x*y) = (a*x)*y by A9,A21;
end;
end;
0.W = 0.V & 1.W= 1.V by A2,A3;
hence thesis by A1,A4,A5,A6,A11,Def9;
end;
registration
let V be Algebra;
cluster strict for Subalgebra of V;
existence
proof
set V1 = [#]V;
A1: the Mult of V = (the Mult of V) | [:REAL,V1:] by RELSET_1:19;
the addF of V = (the addF of V)||V1 & the multF of V = (the multF of V
)||V1 by RELSET_1:19;
then AlgebraStr (# the carrier of V, the multF of V, the addF of V, the
Mult of V, 1.V, 0.V #) is Subalgebra of V by A1,Th3;
hence thesis;
end;
end;
definition
let V be Algebra, V1 be Subset of V;
attr V1 is additively-linearly-closed means
V1 is add-closed
having-inverse & for a be Real, v be Element of V st v in V1 holds a * v in V1;
end;
registration
let V be Algebra;
cluster additively-linearly-closed -> additively-closed for Subset of V;
coherence;
end;
definition
let V be Algebra, V1 be Subset of V such that
A1: V1 is additively-linearly-closed non empty;
func Mult_(V1,V) -> Function of [:REAL,V1:], V1 equals
:Def11:
(the Mult of V) | [:REAL,V1:];
correctness
proof
A2: [:REAL,V1:] c= [:REAL,the carrier of V:] & dom(the Mult of V) = [:REAL
,the carrier of V:] by FUNCT_2:def 1,ZFMISC_1:95;
A3: for z be object st z in [:REAL,V1:] holds ((the Mult of V) | [:REAL,V1:])
.z in V1
proof
let z be object such that
A4: z in [:REAL,V1:];
consider r,x be object such that
A5: r in REAL and
A6: x in V1 and
A7: z=[r,x] by A4,ZFMISC_1:def 2;
reconsider r as Real by A5;
reconsider y=x as VECTOR of V by A6;
[r,x] in dom((the Mult of V) | [:REAL,V1:]) by A2,A4,A7,RELAT_1:62;
then ((the Mult of V) | [:REAL,V1:]).z = r*y by A7,FUNCT_1:47;
hence thesis by A1,A6;
end;
dom((the Mult of V) | [:REAL,V1:]) =[:REAL,V1:] by A2,RELAT_1:62;
hence thesis by A3,FUNCT_2:3;
end;
end;
definition
let V be non empty RLSStruct;
attr V is scalar-mult-cancelable means
for a be Real, v be Element of V st a*v=0.V holds a=0 or v=0.V;
end;
theorem Th4:
for V being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr, a be Real holds a*0.V = 0.V
proof
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non
empty AlgebraStr;
let a be Real;
a * 0.V + a * 0.V = a * (0.V + 0.V) by RLVECT_1:def 5;
then a * 0.V + a * 0.V = a * 0.V;
then a * 0.V + a * 0.V = a * 0.V + 0.V;
hence thesis by RLVECT_1:8;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem
for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr st V is scalar-mult-cancelable
holds V is RealLinearSpace
proof
let V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr;
assume
A1: V is scalar-mult-cancelable;
for v being VECTOR of V holds 1 * v = v
proof
let v be VECTOR of V;
(1*v) + (1 * -v) = 1 * (v + -v) by RLVECT_1:def 5;
then (1*v) - (1*v) = 0.V & (1*v) + (1 * -v) = 1 * 0.V by RLVECT_1:5;
then
A2: -(jj*v) = jj*(-v) by Th4,RLVECT_1:8;
1 * v = (1 * 1) * v .= 1 * (1 * v) by RLVECT_1:def 7;
then 1 * (1 * v) - 1 * v = 0.V by RLVECT_1:15;
then 1 * (1 * v - v) = 0.V by A2,RLVECT_1:def 5;
then (jj*v) - v = 0.V by A1;
hence thesis by RLVECT_1:21;
end;
hence thesis by RLVECT_1:def 8;
end;
Lm2: for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr st for v being VECTOR of V
holds 1 * v = v
holds V is RealLinearSpace by RLVECT_1:def 8;
theorem Th6:
V1 is additively-linearly-closed multiplicatively-closed non
empty implies AlgebraStr(# V1,mult_(V1,V), Add_(V1,V), Mult_(V1,V), One_(V1,V),
Zero_(V1,V) #) is Subalgebra of V
proof
assume
A1: V1 is additively-linearly-closed multiplicatively-closed non empty;
then
A2: Mult_(V1,V) = (the Mult of V) | [:REAL,V1:] by Def11;
A3: One_(V1,V) =1_V & mult_(V1,V) = (the multF of V) || V1 by A1,Def6,Def8;
Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 by A1,Def5,Def7;
hence thesis by A1,A3,A2,Th3;
end;
theorem Th7:
RAlgebra X is RealLinearSpace
proof
for v being VECTOR of RAlgebra X holds 1 * v = v by FUNCSDOM:12;
hence thesis by Lm2;
end;
theorem Th8:
for V be Algebra, V1 be Subalgebra of V holds
( for v1,w1 be Element of V1, v,w be Element of V st v1=v & w1=w
holds v1+w1=v+w ) &
( for v1, w1 be Element of V1, v,w be Element of V st v1=v & w1=w
holds v1*w1=v*w ) & (
for v1 be Element of V1, v be Element of V,
a be Real st v1=v holds a*v1=a*v )
& 1_V1 = 1_V & 0.V1=0.V
proof
let V be Algebra, V1 be Subalgebra of V;
hereby
let x1,y1 be Element of V1, x,y be Element of V;
assume
A1: x1=x & y1=y;
x1 + y1 = ((the addF of V)||the carrier of V1).[x1,y1] by Def9;
hence x1 + y1 = x+y by A1,FUNCT_1:49;
end;
hereby
let x1,y1 be Element of V1, x,y be Element of V;
assume
A2: x1=x & y1=y;
x1 * y1 = ((the multF of V)||the carrier of V1).[x1,y1] by Def9;
hence x1 * y1 = x*y by A2,FUNCT_1:49;
end;
hereby
let v1 be Element of V1, v be Element of V, a be Real;
assume
A3: v1 = v;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
aa * v1 = ((the Mult of V) | [:REAL,the carrier of V1:]).[aa,v1] by Def9;
then aa * v1 = aa * v by A3,FUNCT_1:49;
hence a * v1 = a * v;
end;
thus thesis by Def9;
end;
begin :: Banach Algebra of Bounded Functionals
definition
let X be non empty set;
func BoundedFunctions X -> non empty Subset of RAlgebra X equals
{ f where f is Function of X,REAL : f|X is bounded };
correctness
proof
A1: { f where f is Function of X,REAL : f|X is bounded } is non empty
proof
reconsider g = X --> In(0,REAL) as Function of X,REAL;
g|X is bounded;
then g in { f where f is Function of X,REAL : f|X is bounded };
hence thesis;
end;
{ f where f is Function of X,REAL : f|X is bounded } c= Funcs(X,REAL)
proof
let x be object;
assume x in { f where f is Function of X,REAL : f|X is bounded };
then ex f be Function of X,REAL st x=f & f|X is bounded;
hence thesis by FUNCT_2:8;
end;
hence thesis by A1;
end;
end;
theorem Th9:
BoundedFunctions X is additively-linearly-closed multiplicatively-closed
proof
set W = BoundedFunctions X;
set V = RAlgebra X;
A1: for v,u be Element of V st v in W & u in W holds v * u in W
proof
let v,u be Element of V such that
A2: v in W and
A3: u in W;
consider u1 be Function of X,REAL such that
A4: u1=u and
A5: u1|X is bounded by A3;
reconsider h = v*u as Element of Funcs(X,REAL);
consider v1 be Function of X,REAL such that
A6: v1=v and
A7: v1|X is bounded by A2;
dom(v1(#)u1) = X /\ X by FUNCT_2:def 1;
then
A8: (v1(#)u1)|X is bounded by A7,A5,RFUNCT_1:84;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1;
then
A9: (ex f being Function st h = f & dom f = X & rng f c= REAL)& dom v1 /\
dom u1 = X /\ X by FUNCT_2:def 1,def 2;
for x be object st x in dom h holds h.x = v1.x *u1.x by A6,A4,FUNCSDOM:2;
then v*u=v1(#)u1 by A9,VALUED_1:def 4;
hence thesis by A8;
end;
reconsider g = RealFuncUnit X as Function of X,REAL;
for v,u be Element of V st v in W & u in W holds v + u in W
proof
let v,u be Element of V such that
A10: v in W and
A11: u in W;
consider u1 be Function of X,REAL such that
A12: u1=u and
A13: u1|X is bounded by A11;
reconsider h = v+u as Element of Funcs(X,REAL);
consider v1 be Function of X,REAL such that
A14: v1=v and
A15: v1|X is bounded by A10;
dom(v1+u1) = X /\ X by FUNCT_2:def 1;
then
A16: (v1+u1)|X is bounded by A15,A13,RFUNCT_1:83;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1;
then
A17: (ex f being Function st h = f & dom f = X & rng f c= REAL)& dom v1 /\
dom u1 = X /\ X by FUNCT_2:def 1,def 2;
for x be object st x in dom h holds h.x = v1.x + u1.x
by A14,A12,FUNCSDOM:1;
then v+u=v1+u1 by A17,VALUED_1:def 1;
hence thesis by A16;
end;
then
A18: W is add-closed by IDEAL_1:def 1;
A19: RAlgebra X is RealLinearSpace by Th7;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V;
assume v in W;
then consider v1 be Function of X,REAL such that
A20: v1=v and
A21: v1|X is bounded;
A22: (-v1)|X is bounded by A21,RFUNCT_1:82;
reconsider h = -v, v2 = v as Element of Funcs(X,REAL);
A23: h=(-1)*v by A19,RLVECT_1:16;
A24: now
let x be object;
assume x in dom h;
then reconsider y=x as Element of X;
h.x = (-1)*(v2.y) by A23,FUNCSDOM:4;
hence h.x = -v1.x by A20;
end;
(ex f being Function st h = f & dom f = X & rng f c= REAL)& dom v1 =X
by FUNCT_2:def 1,def 2;
then -v=-v1 by A24,VALUED_1:9;
hence thesis by A22;
end;
then
A25: W is having-inverse;
for a be Real, u be Element of V st u in W holds a * u in W
proof
let a be Real, u be Element of V;
assume u in W;
then consider u1 be Function of X,REAL such that
A26: u1=u and
A27: u1|X is bounded;
A28: (a(#)u1)|X is bounded by A27,RFUNCT_1:80;
reconsider h = a*u as Element of Funcs(X,REAL);
A29: (ex f being Function st h = f & dom f = X & rng f c= REAL)& dom u1 =
X by FUNCT_2:def 1,def 2;
for x be object st x in dom h holds h.x = a*(u1.x) by A26,FUNCSDOM:4;
then a*u=a(#)u1 by A29,VALUED_1:def 5;
hence thesis by A28;
end;
hence BoundedFunctions X is additively-linearly-closed by A18,A25;
g|X is bounded;
then 1.V in W;
hence thesis by A1;
end;
registration
let X;
cluster BoundedFunctions X -> additively-linearly-closed
multiplicatively-closed;
coherence by Th9;
end;
definition
let X be non empty set;
func R_Algebra_of_BoundedFunctions X -> Algebra equals
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 by Th6;
end;
theorem
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
theorem
R_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
now
let v being VECTOR of R_Algebra_of_BoundedFunctions X;
reconsider v1=v as VECTOR of RAlgebra X by TARSKI:def 3;
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
then jj * v = jj*v1 by Th8;
hence 1 * v =v by FUNCSDOM:12;
end;
hence thesis by Lm2;
end;
reserve F,G,H for VECTOR of R_Algebra_of_BoundedFunctions X;
reserve f,g,h for Function of X,REAL;
theorem Th12:
f=F & g=G & h=H implies ( H = F+G iff for x be Element of X
holds h.x = f.x + g.x )
proof
assume
A1: f=F & g=G & h=H;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby
assume
A3: H = F+G;
let x be Element of X;
h1=f1+g1 by A2,A3,Th8;
hence h.x = f.x+g.x by A1,FUNCSDOM:1;
end;
assume for x be Element of X holds h.x = f.x+g.x;
then h1=f1+g1 by A1,FUNCSDOM:1;
hence thesis by A2,Th8;
end;
theorem Th13:
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
assume
A1: f=F & g=G;
reconsider f1=F, g1=G as VECTOR of RAlgebra X by TARSKI:def 3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby
assume
A3: G = a*F;
let x be Element of X;
g1=a*f1 by A2,A3,Th8;
hence g.x=a*f.x by A1,FUNCSDOM:4;
end;
assume for x be Element of X holds g.x=a*f.x;
then g1=a*f1 by A1,FUNCSDOM:4;
hence thesis by A2,Th8;
end;
theorem Th14:
f=F & g=G & h=H implies ( H = F*G iff for x be Element of X
holds h.x = f.x * g.x )
proof
assume
A1: f=F & g=G & h=H;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby
assume
A3: H = F*G;
let x be Element of X;
h1 = f1*g1 by A2,A3,Th8;
hence h.x = f.x * g.x by A1,FUNCSDOM:2;
end;
assume for x be Element of X holds h.x = f.x * g.x;
then h1 = f1 * g1 by A1,FUNCSDOM:2;
hence thesis by A2,Th8;
end;
theorem Th15:
0.R_Algebra_of_BoundedFunctions X = X -->0
proof
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 0.RAlgebra
X = X -->0 by Th6;
hence thesis by Th8;
end;
theorem Th16:
1_R_Algebra_of_BoundedFunctions X = X -->1
proof
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 1_RAlgebra
X = X -->1 by Th6;
hence thesis by Th8;
end;
definition
let X be non empty set, F be object such that
A1: F in BoundedFunctions X;
func modetrans(F,X) -> Function of X,REAL means
:Def15:
it=F & it|X is bounded;
correctness by A1;
end;
definition
let X be non empty set, f be Function of X,REAL;
func PreNorms f -> non empty Subset of REAL equals
the set of all |.f.x.| where x is Element of X ;
coherence
proof
set z = the Element of X;
A1: now
let z be object;
now
assume z in the set of all |.f.x.| where x is Element of X ;
then ex x be Element of X st z=|.f.x.|;
hence z in REAL by XREAL_0:def 1;
end;
hence z in the set of all |.f.x.| where x is Element of X
implies z in REAL;
end;
|.f.z.| in the set of all |.f.x.| where x is Element of X ;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th17:
f|X is bounded implies PreNorms f is bounded_above
proof
assume f|X is bounded;
then consider K be Real such that
A1: for x be object st x in X /\ dom f holds |.f.x.| <= K by RFUNCT_1:73;
A2: X /\ dom f = X /\ X by FUNCT_2:def 1;
take K;
let r be ExtReal;
assume r in PreNorms f;
then ex t be Element of X st r=|.f.t.|;
hence r <=K by A1,A2;
end;
theorem
f|X is bounded iff PreNorms f is bounded_above
proof
now
reconsider K = upper_bound PreNorms f as Real;
assume
A1: PreNorms f is bounded_above;
take K;
now
let t be object;
assume t in X /\ dom f;
then |.f.t.| in PreNorms f;
hence |.f.t.| <= K by A1,SEQ_4:def 1;
end;
hence f|X is bounded by RFUNCT_1:73;
end;
hence thesis by Th17;
end;
definition
let X be non empty set;
func BoundedFunctionsNorm X -> Function of BoundedFunctions X,REAL means
:
Def17: for x be object st x in BoundedFunctions X
holds it.x = upper_bound PreNorms(modetrans(x,X));
existence
proof
deffunc F(object) = upper_bound PreNorms(modetrans($1,X));
A1: for z be object st z in BoundedFunctions X holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of BoundedFunctions X,REAL st for x being object st x
in BoundedFunctions X holds f.x = F(x) from FUNCT_2:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedFunctions X,REAL such that
A2: for x be object st x in BoundedFunctions X holds NORM1.x = upper_bound
PreNorms(modetrans(x,X)) and
A3: for x be object st x in BoundedFunctions X holds NORM2.x = upper_bound
PreNorms(modetrans(x,X));
A4: for z be object st z in BoundedFunctions X holds NORM1.z = NORM2.z
proof
let z be object such that
A5: z in BoundedFunctions X;
NORM1.z = upper_bound PreNorms(modetrans(z,X)) by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = BoundedFunctions X & dom NORM2 = BoundedFunctions X by
FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
theorem Th19:
f|X is bounded implies modetrans(f,X) = f
proof
assume f|X is bounded;
then f in BoundedFunctions X;
hence thesis by Def15;
end;
theorem Th20:
f|X is bounded implies (BoundedFunctionsNorm X).f = upper_bound PreNorms f
proof
reconsider f9=f as set;
assume
A1: f|X is bounded;
then f in BoundedFunctions X;
then (BoundedFunctionsNorm X).f = upper_bound PreNorms(modetrans(f9,X))
by Def17;
hence thesis by A1,Th19;
end;
definition
let X be non empty set;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals
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;
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty;
correctness;
end;
Lm3: now
let X be non empty set;
set F = R_Normed_Algebra_of_BoundedFunctions X;
let x,e be Element of F;
set X1 = BoundedFunctions X;
reconsider f = x as Element of X1;
assume
A1: e = One_(BoundedFunctions X,RAlgebra X);
then x * e = (mult_(X1,RAlgebra X)).(f,1_RAlgebra X) by Def8;
then
A2: x * e = ((the multF of RAlgebra X)||X1).(f,1_RAlgebra X) by Def6;
e * x = (mult_(X1,RAlgebra X)).(1_RAlgebra X,f) by A1,Def8;
then
A3: e * x = ((the multF of RAlgebra X)||X1).(1_RAlgebra X,f) by Def6;
A4: 1_RAlgebra X = 1_R_Algebra_of_BoundedFunctions X by Th16;
then [f,1_RAlgebra X] in [:X1,X1:] by ZFMISC_1:87;
then x * e = f * 1_RAlgebra X by A2,FUNCT_1:49;
hence x * e = x;
[1_RAlgebra X,f] in [:X1,X1:] by A4,ZFMISC_1:87;
then e * x = 1_RAlgebra X * f by A3,FUNCT_1:49;
hence e * x = x;
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> unital;
correctness
proof
reconsider e = One_(BoundedFunctions X,RAlgebra X) as Element of
R_Normed_Algebra_of_BoundedFunctions X;
take e;
thus thesis by Lm3;
end;
end;
theorem Th21:
for W be Normed_AlgebraStr, V be Algebra st the AlgebraStr of W
= V holds W is Algebra
proof
let W be Normed_AlgebraStr,V be Algebra such that
A1: the AlgebraStr of W = V;
reconsider W as non empty AlgebraStr by A1;
A2: W is right_unital
proof
let x being Element of W;
reconsider x1 = x as Element of V by A1;
x*1.W = x1*1.V by A1;
hence thesis;
end;
A3: W is right-distributive
proof
let x,y,z being Element of W;
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
x*(y+z) = x1*(y1+z1) by A1;
then x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 2;
hence thesis by A1;
end;
A4: for x being Element of W holds x is right_complementable
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1;
consider v be Element of V such that
A5: x1 + v = 0.V by ALGSTR_0:def 11;
reconsider y = v as Element of W by A1;
x + y = 0.W by A1,A5;
hence thesis;
end;
A6: for a,b,x being Element of W holds (a * b) * x = a * (b * x)
proof
let a,b,x be Element of W;
reconsider y = x, a1 = a, b1 = b as Element of V by A1;
(a * b) * x = (a1 * b1) * y by A1;
then (a * b) * x = a1 * (b1 * y) by GROUP_1:def 3;
hence thesis by A1;
end;
A7: for v,w being Element of W holds v * w = w * v
proof
let v,w being Element of W;
reconsider v1 = v, w1 = w as Element of V by A1;
v * w = v1*w1 by A1;
then v * w = w1*v1;
hence thesis by A1;
end;
A8: for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
(x + y) + z = (x1 + y1) + z1 by A1;
then (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 3;
hence thesis by A1;
end;
A9: for x,y being VECTOR of W holds x + y = y + x
proof
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1;
x + y = x1+y1 by A1;
then x + y =y1 + x1;
hence thesis by A1;
end;
A10: W is vector-distributive
proof
let a be Real;
let x,y being Element of W;
reconsider x1 = x, y1 = y as Element of V by A1;
a*(x+y) = a*(x1+y1) by A1;
then a*(x+y) = a*x1 + a*y1 by RLVECT_1:def 5;
hence a*(x+y) = a*x + a*y by A1;
end;
A11: W is scalar-distributive
proof
let a,b be Real;
let x being Element of W;
reconsider x1 = x as Element of V by A1;
(a+b)*x = (a+b)*x1 by A1;
then (a+b)*x = a*x1 + b*x1 by RLVECT_1:def 6;
hence (a+b)*x =a*x + b*x by A1;
thus thesis;
end;
A12: W is scalar-associative
proof
let a,b be Real;
let x being Element of W;
reconsider x1 = x as Element of V by A1;
(a*b)*x = (a*b)*x1 by A1;
then (a*b)*x = a*(b*x1) by RLVECT_1:def 7;
hence thesis by A1;
end;
A13: W is vector-associative
proof
let x,y being Element of W;
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Real;
a*(x*y) = a*(x1*y1) by A1;
then a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 9;
hence a*(x*y) = (a*x)*y by A1;
end;
for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1;
x + 0.W = y + 0.V by A1;
hence thesis;
end;
hence thesis by A9,A8,A4,A7,A6,A2,A3,A10,A11,A12,A13,ALGSTR_0:def 16
,GROUP_1:def 3,def 12,RLVECT_1:def 2,def 3,def 4;
end;
reserve F,G,H for Point of R_Normed_Algebra_of_BoundedFunctions X;
theorem Th22:
R_Normed_Algebra_of_BoundedFunctions X is Algebra
proof
1.(R_Normed_Algebra_of_BoundedFunctions X) =
1_R_Algebra_of_BoundedFunctions X;
hence thesis by Th21;
end;
theorem Th23:
(Mult_(BoundedFunctions X,RAlgebra X)).(1,F) = F
proof
set X1 = BoundedFunctions X;
reconsider f1 = F as Element of X1;
A1: [jj,f1] in [:REAL,X1:];
thus (Mult_(BoundedFunctions X,RAlgebra X)).(1,F) = ((the Mult of RAlgebra X
)| [:REAL,X1:]).(1,f1) by Def11
.= (the Mult of RAlgebra X).(1,f1) by A1,FUNCT_1:49
.= F by FUNCSDOM:12;
end;
theorem Th24:
R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
(for v being VECTOR of R_Normed_Algebra_of_BoundedFunctions X holds 1 *
v = v)& R_Normed_Algebra_of_BoundedFunctions X is Algebra by Th22,Th23;
hence thesis by Lm2;
end;
theorem Th25:
X-->0 = 0.R_Normed_Algebra_of_BoundedFunctions X
proof
X-->0 = 0.R_Algebra_of_BoundedFunctionsX by Th15;
hence thesis;
end;
theorem Th26:
f=F & f|X is bounded implies |.f.x.| <= ||.F.||
proof
assume that
A1: f=F and
A2: f|X is bounded;
A3: |.f.x.| in PreNorms f;
PreNorms f is non empty bounded_above by A2,Th17;
then |.f.x.| <= upper_bound PreNorms f by A3,SEQ_4:def 1;
hence thesis by A1,A2,Th20;
end;
theorem
0 <= ||.F.||
proof
F in BoundedFunctions X;
then consider g be Function of X,REAL such that
A1: F=g and
A2: g|X is bounded;
A3: PreNorms g is non empty bounded_above by A2,Th17;
consider r0 be object such that
A4: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A4;
now
let r be Real;
assume r in PreNorms g;
then ex t be Element of X st r=|.g.t.|;
hence 0 <= r by COMPLEX1:46;
end;
then 0 <= r0 by A4;
then 0 <=upper_bound PreNorms g by A3,A4,SEQ_4:def 1;
hence thesis by A1,A2,Th20;
end;
theorem Th28:
F = 0.R_Normed_Algebra_of_BoundedFunctions X implies 0 = ||.F.||
proof
set z = X --> In(0,REAL);
reconsider z as Function of X, REAL;
F in BoundedFunctions X;
then consider g be Function of X,REAL such that
A1: g=F and
A2: g|X is bounded;
A3: PreNorms g is non empty bounded_above by A2,Th17;
consider r0 be object such that
A4: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A4;
A5: (for s be Real st s in PreNorms g holds s <= 0) implies upper_bound
PreNorms g <= 0 by SEQ_4:45;
assume
A6: F = 0.R_Normed_Algebra_of_BoundedFunctions X;
A7: now
let r be Real;
assume r in PreNorms g;
then consider t be Element of X such that
A8: r=|.g.t.|;
z=g by A6,A1,Th25;
then |.g.t.| = |.0 .|;
hence 0 <= r & r <=0 by A8,ABSVALUE:2;
end;
then 0 <= r0 by A4;
then upper_bound PreNorms g = 0 by A7,A3,A4,A5,SEQ_4:def 1;
hence thesis by A1,A2,Th20;
end;
theorem Th29:
f=F & g=G & h=H implies (H = F+G iff for x be Element of X holds
h.x = f.x + g.x)
proof
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_BoundedFunctions X;
A1: H=F+G iff h1=f1+g1;
assume f=F & g=G & h=H;
hence thesis by A1,Th12;
end;
theorem Th30:
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
reconsider f1=F, g1=G as VECTOR of R_Algebra_of_BoundedFunctions X;
A1: G=a*F iff g1=a*f1;
assume f=F & g=G;
hence thesis by A1,Th13;
end;
theorem Th31:
f=F & g=G & h=H implies (H = F*G iff for x be Element of X holds
h.x = f.x * g.x)
proof
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_BoundedFunctions X;
A1: H=F*G iff h1=f1*g1;
assume f=F & g=G & h=H;
hence thesis by A1,Th14;
end;
theorem Th32:
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_BoundedFunctions X )
& ||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
A1: now
set z = X --> In(0,REAL);
reconsider z as Function of X,REAL;
F in BoundedFunctions X;
then consider g be Function of X,REAL such that
A2: F=g and
A3: g|X is bounded;
A4: PreNorms g is non empty bounded_above by A3,Th17;
consider r0 be object such that
A5: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A5;
A6: (for s be Real st s in PreNorms g holds s <= 0) implies upper_bound
PreNorms g <= 0 by SEQ_4:45;
assume F = 0.R_Normed_Algebra_of_BoundedFunctions X;
then
A7: z=g by A2,Th25;
A8: now
let r be Real;
assume r in PreNorms g;
then consider t be Element of X such that
A9: r=|.g.t.|;
|.g.t.| = |.0 .| by A7
.= 0 by ABSVALUE:2;
hence 0 <= r & r <=0 by A9;
end;
then 0<=r0 by A5;
then upper_bound PreNorms g = 0 by A8,A4,A5,A6,SEQ_4:def 1;
hence ||.F.|| = 0 by A2,A3,Th20;
end;
A10: ||.F+G.|| <= ||.F.|| + ||.G.||
proof
F+G in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A11: h1=F+G and
A12: h1|X is bounded;
G in BoundedFunctions X;
then consider g1 be Function of X,REAL such that
A13: g1=G and
A14: g1|X is bounded;
F in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A15: f1=F and
A16: f1|X is bounded;
A17: now
let t be Element of X;
|.f1.t.| <= ||.F.|| & |.g1.t.|<= ||.G.|| by A15,A16,A13,A14,Th26;
then
A18: |.f1.t.| +|.g1.t.| <= ||.F.|| + ||.G.|| by XREAL_1:7;
|.h1.t.| =|.f1.t+g1.t.| & |.f1.t+g1.t.| <=|.f1.t.| +|.g1.t.|
by A15,A13,A11,Th29,COMPLEX1:56;
hence |.h1.t.| <= ||.F.|| + ||.G.|| by A18,XXREAL_0:2;
end;
A19: now
let r be Real;
assume r in PreNorms h1;
then ex t be Element of X st r=|.h1.t.|;
hence r <= ||.F.|| + ||.G.|| by A17;
end;
(for s be Real st s in PreNorms h1 holds s <= ||.F.|| + ||.G
.||) implies upper_bound PreNorms h1 <= ||.F.|| + ||.G.|| by SEQ_4:45;
hence thesis by A11,A12,A19,Th20;
end;
A20: ||.a*F.|| = |.a.| * ||.F.||
proof
F in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A21: f1=F and
A22: f1|X is bounded;
a*F in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A23: h1=a*F and
A24: h1|X is bounded;
A25: now
let t be Element of X;
|.h1.t.| = |.a*f1.t.| by A21,A23,Th30;
then
A26: |.h1.t.| = |.a.| * |.f1.t.| by COMPLEX1:65;
0<= |.a.| by COMPLEX1:46;
hence |.h1.t.| <= |.a.| *||.F.|| by A21,A22,A26,Th26,XREAL_1:64;
end;
A27: now
let r be Real;
assume r in PreNorms h1;
then ex t be Element of X st r=|.h1.t.|;
hence r <= |.a.| *||.F.|| by A25;
end;
(for s be Real st s in PreNorms h1 holds s <= |.a.| *||.F.|| )
implies upper_bound PreNorms h1 <= |.a.| *||.F.|| by SEQ_4:45;
then
A28: ||.a*F.|| <= |.a.| *||.F.|| by A23,A24,A27,Th20;
per cases;
suppose
A29: a <> 0;
A30: now
let t be Element of X;
|.a".| =|.1/a.|;
then
A31: |.a".| =1/|.a.| by ABSVALUE:7;
h1.t=a*f1.t by A21,A23,Th30;
then a"*h1.t = (a"* a)*f1.t;
then
A32: a"*h1.t =1*f1.t by A29,XCMPLX_0:def 7;
|.a"*h1.t.| = |.a".|*|.h1.t.| & 0 <= |.a".| by COMPLEX1:46,65;
hence |.f1.t.| <= |.a.|"*||.a*F.|| by A23,A24,A32,A31,Th26,XREAL_1:64;
end;
A33: now
let r be Real;
assume r in PreNorms f1;
then ex t be Element of X st r=|.f1.t.|;
hence r <= |.a.|"*||.a*F.|| by A30;
end;
A34: 0 <= |.a.| by COMPLEX1:46;
(for s be Real st s in PreNorms f1 holds s <= |.a.|"*||.a*F
.||) implies upper_bound PreNorms f1 <= |.a.|"*||.a*F.|| by SEQ_4:45;
then ||.F.|| <=|.a.|"*||.a*F.|| by A21,A22,A33,Th20;
then |.a.|*||.F.|| <=|.a.|*(|.a.|"*||.a*F.||) by A34,XREAL_1:64;
then
A35: |.a.|*||.F.|| <=(|.a.|*|.a.|")*||.a*F.||;
|.a.| <>0 by A29,COMPLEX1:47;
then |.a.|*||.F.|| <=1*||.a*F.|| by A35,XCMPLX_0:def 7;
hence thesis by A28,XXREAL_0:1;
end;
suppose
A36: a=0;
reconsider fz=F as VECTOR of R_Algebra_of_BoundedFunctions X;
a*fz =(a+a)*fz by A36
.=a*fz + a* fz by RLVECT_1:def 6;
then 0.R_Algebra_of_BoundedFunctions X = -(a*fz)+(a*fz + a* fz) by
VECTSP_1:16;
then 0.R_Algebra_of_BoundedFunctions X = -(a*fz)+a*fz + a* fz by
RLVECT_1:def 3;
then
0.R_Algebra_of_BoundedFunctions X = 0.R_Algebra_of_BoundedFunctions
X + a * fz by VECTSP_1:16;
then
A37: a*F =0.R_Normed_Algebra_of_BoundedFunctions X;
|.a.|* ||.F.|| =0 * ||.F.|| by A36,ABSVALUE:2;
hence thesis by A37,Th28;
end;
end;
now
set z = X --> In(0,REAL);
reconsider z as Function of X,REAL;
F in BoundedFunctions X;
then consider g be Function of X,REAL such that
A38: F=g and
A39: g|X is bounded;
assume
A40: ||.F.|| = 0;
now
let t be Element of X;
|.g.t.| <= ||.F.|| by A38,A39,Th26;
then |.g.t.| = 0 by A40,COMPLEX1:46;
hence g.t =0 by ABSVALUE:2
.=z.t;
end;
then g=z by FUNCT_2:63;
hence F=0.R_Normed_Algebra_of_BoundedFunctions X by A38,Th25;
end;
hence thesis by A1,A20,A10;
end;
theorem Th33:
R_Normed_Algebra_of_BoundedFunctions X is
reflexive discerning RealNormSpace-like
proof
thus ||.0.R_Normed_Algebra_of_BoundedFunctions X.|| = 0 by Th32;
for x, y being Point of R_Normed_Algebra_of_BoundedFunctions X for a be
Real
holds ( ||.x.|| = 0 iff x = 0.R_Normed_Algebra_of_BoundedFunctions(X) ) &
||.a*x.|| = |.a.| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th32;
hence thesis by NORMSP_1:def 1;
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Th24,Th33;
end;
theorem Th34:
f=F & g=G & h=H implies (H = F-G iff for x be Element of X holds
h.x = f.x - g.x )
proof
assume
A1: f=F & g=G & h=H;
A2: now
assume
A3: for x be Element of X holds h.x = f.x - g.x;
now
let x be Element of X;
h.x = f.x - g.x by A3;
hence h.x + g.x= f.x;
end;
then F=H+G by A1,Th29;
then F-G=H+(G-G) by RLVECT_1:def 3;
then F-G=H+0.R_Normed_Algebra_of_BoundedFunctions X by RLVECT_1:15;
hence F-G=H;
end;
now
assume H=F-G;
then H+G=F-(G-G) by RLVECT_1:29;
then H+G=F-0.R_Normed_Algebra_of_BoundedFunctions X by RLVECT_1:15;
then
A4: H+G=F;
now
let x be Element of X;
f.x=h.x + g.x by A1,A4,Th29;
hence f.x-g.x=h.x;
end;
hence for x be Element of X holds h.x = f.x - g.x;
end;
hence thesis by A2;
end;
theorem Th35:
for X be non empty set for seq be sequence of
R_Normed_Algebra_of_BoundedFunctions X st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty set;
let vseq be sequence of R_Normed_Algebra_of_BoundedFunctions X;
defpred P[set,set] means ex xseq be Real_Sequence st
(for n be Nat holds xseq.n=modetrans(vseq.n,X).$1) &
xseq is convergent & $2= lim xseq;
assume
A1: vseq is Cauchy_sequence_by_Norm;
A2: for x be Element of X ex y be Element of REAL st P[x,y]
proof
let x be Element of X;
deffunc F(Nat) = modetrans(vseq.$1,X).x;
consider xseq be Real_Sequence such that
A3: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4;
A4: for n be Nat holds xseq.n = F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
reconsider lx = lim xseq as Element of REAL by XREAL_0:def 1;
take lx;
A5: for m,k be Nat holds |.xseq.m-xseq.k.| <= ||.vseq.m - vseq.k.||
proof
let m,k be Nat;
vseq.m-vseq.k in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A6: h1=vseq.m-vseq.k and
A7: h1|X is bounded;
vseq.m in BoundedFunctions X;
then
ex vseqm be Function of X,REAL st vseq.m=vseqm & vseqm|X is bounded;
then
A8: modetrans(vseq.m,X)=vseq.m by Th19;
vseq.k in BoundedFunctions X;
then
ex vseqk be Function of X,REAL st vseq.k=vseqk & vseqk|X is bounded;
then
A9: modetrans(vseq.k,X)=vseq.k by Th19;
xseq.m =modetrans(vseq.m,X).x & xseq.k =modetrans(vseq.k,X).x by A4;
then xseq.m - xseq.k = h1.x by A8,A9,A6,Th34;
hence thesis by A6,A7,Th26;
end;
now
let e be Real such that
A10: e > 0;
consider k be Nat such that
A11: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n)
- (vseq.m).|| < e by A1,A10,RSSPACE3:8;
take k;
let n be Nat;
assume n >=k;
then
A12: ||. vseq.n - vseq.k .|| < e by A11;
|.xseq.n-xseq.k.| <= ||. vseq.n - vseq.k .|| by A5;
hence |.xseq.n-xseq.k.| < e by A12,XXREAL_0:2;
end;
then xseq is convergent by SEQ_4:41;
hence thesis by A4;
end;
consider tseq be Function of X,REAL such that
A13: for x be Element of X holds P[x,tseq.x] from FUNCT_2:sch 3(A2);
now
let e1 be Real such that
A14: e1 >0;
reconsider e =e1 as Real;
consider k be Nat such that
A15: for n,m be Nat st n >= k & m >= k holds ||. vseq.n -
vseq.m .|| < e by A1,A14,RSSPACE3:8;
take k;
let m be Nat;
A16: ||.vseq.m.||= ||.vseq.||.m by NORMSP_0:def 4;
assume m >= k;
then
A17: ||. vseq.m - vseq.k .|| <e by A15;
|.||.vseq.m.||- ||.vseq.k.||.| <= ||. vseq.m - vseq.k .|| & ||.vseq
.k.||= ||.vseq.||.k by NORMSP_0:def 4,NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| < e1 by A17,A16,XXREAL_0:2;
end;
then
A18: ||.vseq.|| is convergent by SEQ_4:41;
now
let x be object;
assume
A19: x in X /\ dom tseq;
then consider xseq be Real_Sequence such that
A20: for n be Nat holds xseq.n=modetrans(vseq.n,X).x and
A21: xseq is convergent & tseq.x = lim xseq by A13;
A22: for n be Nat holds abs(xseq).n <= ||.vseq.|| .n
proof
let n be Nat;
A23: xseq.n =modetrans(vseq.n,X).x by A20;
vseq.n in BoundedFunctions X;
then
A24: ex h1 be Function of X,REAL st vseq.n=h1 & h1|X is bounded;
then modetrans(vseq.n,X)=vseq.n by Th19;
then |.xseq.n.| <= ||.vseq.n.|| by A19,A24,A23,Th26;
then abs(xseq).n <= ||.vseq.n.|| by VALUED_1:18;
hence thesis by NORMSP_0:def 4;
end;
abs xseq is convergent & |.tseq.x.| = lim abs(xseq) by A21,SEQ_4:14;
hence |.tseq.x.| <= lim ||.vseq.|| by A18,A22,SEQ_2:18;
end;
then tseq|X is bounded by RFUNCT_1:73;
then tseq in BoundedFunctions X;
then reconsider tv=tseq as Point of R_Normed_Algebra_of_BoundedFunctions X;
A25: for e be Real st e > 0
ex k be Nat st
for n be Nat st n >= k
for x be Element of X holds |.modetrans(vseq.n,X).x -
tseq.x.| <= e
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A26: for n,m be Nat st n >= k & m >= k holds ||. vseq.n -
vseq.m .|| < e by A1,RSSPACE3:8;
take k;
let n be Nat such that
A27: n >= k;
now
let x be Element of X;
consider xseq be Real_Sequence such that
A28: for n be Nat holds xseq.n=modetrans(vseq.n,X).x and
A29: xseq is convergent and
A30: tseq.x = lim xseq by A13;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
set fseq = seq_const xseq.n;
set wseq = xseq-fseq;
deffunc F(Nat) = |.xseq.$1 - xseq.n.|;
consider rseq be Real_Sequence such that
A31: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
A32: for m,k be Nat holds |.xseq.m-xseq.k.| <= ||.vseq.m -
vseq.k.||
proof
let m,k be Nat;
vseq.m-vseq.k in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A33: h1 =vseq.m-vseq.k and
A34: h1|X is bounded;
vseq.m in BoundedFunctions X;
then ex vseqm be Function of X,REAL st vseq.m=vseqm & vseqm|X is
bounded;
then
A35: modetrans(vseq.m,X) = vseq.m by Th19;
vseq.k in BoundedFunctions X;
then ex vseqk be Function of X,REAL st vseq.k=vseqk & vseqk|X is
bounded;
then
A36: modetrans(vseq.k,X)=vseq.k by Th19;
xseq.m =modetrans(vseq.m,X).x & xseq.k =modetrans((vseq.k),X).x
by A28;
then xseq.m - xseq.k =h1.x by A35,A36,A33,Th34;
hence thesis by A33,A34,Th26;
end;
A37: for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat;
assume m >=k;
then
A38: ||.vseq.n - vseq.m.|| <e by A26,A27;
rseq.m = |.xseq.m-xseq.n.| by A31;
then rseq.m = |.xseq.n-xseq.m.| by COMPLEX1:60;
then rseq.m <= ||.vseq.n - vseq.m.|| by A32;
hence thesis by A38,XXREAL_0:2;
end;
A39: now
let m be Element of NAT;
wseq.m = xseq.m +(-fseq).m by SEQ_1:7;
then wseq.m = xseq.m +-fseq.m by SEQ_1:10;
hence wseq.m = xseq.m - xseq.n by SEQ_1:57;
end;
now
let x be object;
assume x in NAT;
then reconsider k=x as Element of NAT;
rseq.x = |.xseq.k - xseq.n.| by A31;
then rseq.x = |.wseq.k.| by A39;
hence rseq.x = abs(wseq).x by VALUED_1:18;
end;
then
A40: rseq = abs(wseq) by FUNCT_2:12;
A41: wseq is convergent by A29;
then rseq is convergent by A40;
then
A42: lim rseq <= e by A37,RSSPACE2:5;
lim fseq = fseq.0 by SEQ_4:26;
then lim fseq =xseq.n by SEQ_1:57;
then lim wseq= tseq.x - xseq.n by A29,A30,SEQ_2:12;
then lim rseq = |.tseq.x-xseq.n.| by A41,A40,SEQ_4:14;
then |.xseq.n-tseq.x.| <= e by A42,COMPLEX1:60;
hence |.modetrans(vseq.n,X).x - tseq.x.| <= e by A28;
end;
hence for x be Element of X holds |.modetrans(vseq.n,X).x - tseq.x.| <=
e;
end;
A43: for e be Real st e > 0
ex k be Element of NAT st for n be Element of NAT
st n >= k holds ||.vseq.n - tv.|| <= e
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A44: for n be Nat st n >= k holds for x be Element of X
holds |.modetrans((vseq.n),X).x - tseq.x.| <= e by A25;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
hereby
let n be Element of NAT such that
A45: n >= k;
vseq.n in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A46: f1=vseq.n and
f1|X is bounded;
vseq.n-tv in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A47: h1=vseq.n-tv and
A48: h1|X is bounded;
A49: now
let t be Element of X;
modetrans(vseq.n,X)=f1 & h1.t = f1.t- tseq.t by A46,A47,Def15,Th34;
hence |.h1.t.| <=e by A44,A45;
end;
A50: now
let r be Real;
assume r in PreNorms h1;
then ex t be Element of X st r=|.h1.t.|;
hence r <=e by A49;
end;
(for s be Real st s in PreNorms h1 holds s <= e) implies
upper_bound PreNorms h1 <= e by SEQ_4:45;
hence ||.vseq.n-tv.|| <=e by A47,A48,A50,Th20;
end;
end;
for e be Real st e > 0 ex m be Nat st
for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A51: e > 0;
reconsider ee=e as Real;
consider m be Element of NAT such that
A52: for n be Element of NAT st n >= m holds ||.(vseq.n) - tv.|| <= ee
/2 by A43,A51,XREAL_1:215;
take m;
A53: e/2<e by A51,XREAL_1:216;
let n be Nat;
A54: n in NAT by ORDINAL1:def 12;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 by A52,A54;
hence ||.(vseq.n) - tv.|| < e by A53,XXREAL_0:2;
end;
hence thesis by NORMSP_1:def 6;
end;
theorem Th36:
R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
proof
for seq be sequence of R_Normed_Algebra_of_BoundedFunctions X st seq is
Cauchy_sequence_by_Norm holds seq is convergent by Th35;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> complete;
coherence by Th36;
end;
registration let X;
cluster R_Normed_Algebra_of_BoundedFunctions X
-> Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital;
coherence
proof set B = R_Normed_Algebra_of_BoundedFunctions X;
thus B is Banach_Algebra-like_1
proof
let f,g being Element of B;
f in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A1: f1=f and
A2: f1|X is bounded;
g in BoundedFunctions X;
then consider g1 be Function of X,REAL such that
A3: g1=g and
A4: g1|X is bounded;
A5: PreNorms g1 is non empty bounded_above by A4,Th17;
f*g in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A6: h1=f*g and
A7: h1|X is bounded;
A8: PreNorms f1 is non empty bounded_above by A2,Th17;
now
let s be Real;
assume s in PreNorms h1;
then consider t be Element of X such that
A9: s = |.h1.t.|;
|.g1.t.| in PreNorms g1;
then
A10: |.g1.t.| <= upper_bound PreNorms g1 by A5,SEQ_4:def 1;
|.f1.t.| in PreNorms f1;
then
A11: |.f1.t.| <= upper_bound PreNorms f1 by A8,SEQ_4:def 1;
0 <= |.f1.t.| by COMPLEX1:46;
then 0 <= upper_bound PreNorms f1 by A11;
then
A12: (upper_bound PreNorms f1)*|.g1.t.| <= (upper_bound PreNorms f1)*(
upper_bound PreNorms g1) by A10,XREAL_1:64;
0 <= |.g1.t.| by COMPLEX1:46;
then
A13: |.f1.t.|*|.g1.t.| <= (upper_bound PreNorms f1)*|.g1.t.|
by A11,XREAL_1:64;
|.h1.t.| = |.f1.t * g1.t.| by A1,A3,A6,Th31;
then |.h1.t.| = |.f1.t.|*|.g1.t.| by COMPLEX1:65;
hence s <= (upper_bound PreNorms f1)*(upper_bound PreNorms g1) by A9,A13
,A12,XXREAL_0:2;
end;
then
A14: upper_bound PreNorms h1 <= (upper_bound PreNorms f1)*(upper_bound
PreNorms g1) by SEQ_4:45;
A15: ||.g.|| = upper_bound PreNorms g1 by A3,A4,Th20;
||.f.|| = upper_bound PreNorms f1 by A1,A2,Th20;
hence ||. f*g .|| <= ||.f.|| * ||.g.|| by A6,A7,A15,A14,Th20;
end;
1.B in BoundedFunctions X;
then consider ONE be Function of X,REAL such that
A16: ONE = 1.B and
A17: ONE|X is bounded;
1.B = 1_R_Algebra_of_BoundedFunctions X;
then
A18: 1.B = X --> 1 by Th16;
for s be object holds s in PreNorms ONE iff s = 1
proof
set t = the Element of X;
let s be object;
hereby
assume s in PreNorms ONE;
then consider t be Element of X such that
A20: s = |.ONE.t.|;
A21: s = |.(X-->1).t.| by A16,A18,A20;
thus s = 1 by A21,COMPLEX1:48;
end;
assume s = 1;
then s = |.(X-->1).t.| by COMPLEX1:48;
hence thesis by A16,A18;
end;
then PreNorms ONE = {1} by TARSKI:def 1;
then upper_bound PreNorms ONE = 1 by SEQ_4:9;
then ||. 1.B .|| = 1 by A16,A17,Th20;
hence B is Banach_Algebra-like_2;
thus B is Banach_Algebra-like_3
proof
let a be Real, f,g be Element of B;
f in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A22: f1=f and
f1|X is bounded;
g in BoundedFunctions X;
then consider g1 be Function of X,REAL such that
A23: g1=g and
g1|X is bounded;
a*(f*g) in BoundedFunctions X;
then consider h3 be Function of X,REAL such that
A24: h3=a*(f*g) and
h3|X is bounded;
f*g in BoundedFunctions X;
then consider h2 be Function of X,REAL such that
A25: h2=f*g and
h2|X is bounded;
a*g in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A26: h1=a*g and
h1|X is bounded;
now
let x be Element of X;
h3.x = a*h2.x by A25,A24,Th30;
then h3.x = a * (f1.x * g1.x) by A22,A23,A25,Th31;
then h3.x = f1.x * (a * g1.x);
hence h3.x = f1.x * h1.x by A23,A26,Th30;
end;
hence a*(f*g) = f*(a*g) by A22,A26,A24,Th31;
end;
thus B is left-distributive
proof
let f,g,h be Element of B;
f in BoundedFunctions X;
then consider f1 be Function of X,REAL such that
A27: f1=f and
f1|X is bounded;
h in BoundedFunctions X;
then consider h1 be Function of X,REAL such that
A28: h1=h and
h1|X is bounded;
g in BoundedFunctions X;
then consider g1 be Function of X,REAL such that
A29: g1=g and
g1|X is bounded;
(g+h)*f in BoundedFunctions X;
then consider F1 be Function of X,REAL such that
A30: F1=(g+h)*f and
F1|X is bounded;
h*f in BoundedFunctions X;
then consider hf1 be Function of X,REAL such that
A31: hf1=h*f and
hf1|X is bounded;
g*f in BoundedFunctions X;
then consider gf1 be Function of X,REAL such that
A32: gf1=g*f and
gf1|X is bounded;
g+h in BoundedFunctions X;
then consider gPh1 be Function of X,REAL such that
A33: gPh1=g+h and
gPh1|X is bounded;
now
let x be Element of X;
F1.x = gPh1.x * f1.x by A27,A33,A30,Th31;
then F1.x = (g1.x + h1.x) * f1.x by A29,A28,A33,Th29;
then F1.x = g1.x * f1.x + h1.x * f1.x;
then F1.x = gf1.x + h1.x * f1.x by A27,A29,A32,Th31;
hence F1.x = gf1.x + hf1.x by A27,A28,A31,Th31;
end;
hence (g+h)*f = g*f + h*f by A32,A31,A30,Th29;
end;
thus for f be Element of B holds 1.B * f = f by Lm3;
end;
end;
theorem
R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
by Th22;