:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1,
VECTSP_2, REALSET1, SEQ_1, BOOLE, RFUNCT_1, FUNCOP_1, LATTICES, SEQ_2,
ABSVALUE, FUNCSDOM, LOPBAN_1, ORDINAL2, ARYTM_3, PARTFUN2, ARYTM,
BINOP_1, ALGSTR_0, NORMSP_1, FUNCT_2, SEQM_3, BHSP_3, RSSPACE4, GROUP_1,
PRE_TOPC, LOPBAN_2, C0SP1, ALGSTR_2, IDEAL_1, SUBSET_1, POLYALG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, REALSET1, FUNCT_1,
FUNCT_2, BINOP_1, DOMAIN_1, RELSET_1, PRE_TOPC, BINOP_2, RLVECT_1,
GROUP_1, VECTSP_1, FRAENKEL, FUNCSDOM, PARTFUN1, PARTFUN2, IDEAL_1,
RSSPACE, RSSPACE3, RCOMP_1, PSCOMP_1, VALUED_1, SEQ_1, XXREAL_0,
RFUNCT_1, SEQ_2, SEQ_4, PRE_CIRC, RLSUB_1, NORMSP_1, SEQM_3, LOPBAN_1,
LOPBAN_2;
constructors REAL_1, REALSET1, PRE_CIRC, PARTFUN2, RSSPACE3, COMPLEX1,
RFUNCT_3, PSCOMP_1, NAT_1, BINOP_2, RCOMP_1, RLSUB_1, LOPBAN_2, ALGSTR_1,
FUNCT_2, VALUED_1, SEQ_1, SEQ_2, ALGSTR_0, IDEAL_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, RELAT_1, XXREAL_0,
RLVECT_1, VECTSP_1, VECTSP_2, FUNCT_2, VALUED_0, VALUED_1, LOPBAN_2,
GCD_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions PRE_TOPC, PSCOMP_1, REALSET1, ALGSTR_0, TARSKI, ORDINAL1,
XCMPLX_0, FINSET_1, REAL_1, FUNCT_2, MEMBERED, ZFMISC_1, NORMSP_1,
FINSEQ_1, GOBOARD1, PARTFUN1, SEQ_4, RFUNCT_1, FUNCSDOM, RLVECT_1,
RLSUB_1, RSSPACE, RSSPACE3, VECTSP_1, VECTSP_2, STRUCT_0, GROUP_1,
BINOP_1, LOPBAN_2, VALUED_1;
theorems STRUCT_0, SEQM_3, SEQ_4, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE,
ALGSTR_0, COMPLEX1, ZFMISC_1, TARSKI, RSSPACE3, RELAT_1, XREAL_0,
XXREAL_0, PARTFUN2, FUNCSDOM, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0,
XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, GROUP_1, LOPBAN_2,
VALUED_1, RSSPACE2, IDEAL_1;
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 :Rdef210b:
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 :Rdef210:
V1 is add-closed having-inverse;
end;
Cor1:
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 [#]V is add-closed by IDEAL_1:def 1;
end;
Cor2:
for V be non empty addLoopStr holds [#]V is having-inverse
proof
let V be non empty addLoopStr;
for v be Element of V st v in [#]V holds -v in [#]V;
hence [#]V is having-inverse by Rdef210b;
end;
registration
let V be non empty addLoopStr;
cluster [#]V -> add-closed having-inverse;
correctness by Cor1,Cor2;
end;
registration
let V be non empty doubleLoopStr;
cluster additively-closed -> add-closed having-inverse Subset of V;
coherence by Rdef210;
cluster add-closed having-inverse -> additively-closed Subset of V;
coherence by Rdef210;
end;
registration
let V be non empty addLoopStr;
cluster add-closed having-inverse non empty Subset of V;
correctness
proof
take [#]V;
thus thesis;
end;
end;
definition let V be Ring;
mode Subring of V -> Ring means :DefSubRing:
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 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 &
1.V =1.V & 0.V = 0.V by FUNCT_2:40;
end;
end;
reserve X for non empty set;
reserve x for Element of X;
reserve d1,d2,a,b 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 Th01:
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
A3: A = (the addF of V)||V1 and
A4: M = (the multF of V)||V1 and
A0: d1 = 1.V and
A2: d2 = 0.V and
B0: 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;
A5:0.W = 0.V & 1.W = 1.V by A2,A0;
A6:now let x,y be Element of W;
x + y = (the addF of V).([x,y]) by A1,A3,FUNCT_1:72;
hence x + y = (the addF of V).(x,y);
end;
A7:now let a,x be Element of W;
a*x = (the multF of V).([a,x]) by A1,A4,FUNCT_1:72;
hence a*x = (the multF of V).(a,x);
end;
W is Abelian add-associative right_zeroed right_complementable
associative well-unital distributive
proof
set Av = the addF of V;
set MV = the multF 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 A6;
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.(x +y,z1) & x + (y + z) = Av.(x1,y + z) by A6; then
(x + y) + z = (x1 + y1) + z1 & x + (y + z) = x1 + (y1 + z1) by A6;
hence (x + y) + z = x + (y + z) by RLVECT_1:def 6;
end;
hereby let x be Element of W;
reconsider y = x, z = 0.W as Element of V by A1,TARSKI:def 3;
x + 0.W = y + 0.V by A2,A6;
hence x + 0.W = x by RLVECT_1:10;
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
A8: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A8,VECTSP_1:63; then
reconsider y = v as Element of W by A1,B0;
take y;
thus x + y = 0.W by A2,A6,A8;
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 = a1 * b1 & a * (b * x) = MV.(a,b * x) by A7; then
(a * b) * x = (a1 * b1) * y & a * (b * x) = a1 * (b1 * y) by A7;
hence (a * b) * x = a * (b * x) by GROUP_1:def 4;
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 A0,A7;
hence x*1.W = x & 1.W * x =x by VECTSP_1:def 16;
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;
a*(x+y) = MV.(a,x+y) & (x+y)*a = MV.(x+y,a) by A7; then
a*(x+y) = a1*(x1+y1) & (x+y)*a = (x1+y1)*a1 by A6; then
a*(x+y) = a1*x1 + a1*y1 & (x+y)*a = x1*a1 + y1*a1 by VECTSP_1:def 18; then
a*(x+y) = Av.(MV.(a,x1),a*y) & (x+y)*a = Av.(MV.(x1,a1),y*a) by A7; then
a*(x+y) = Av.(a*x,a*y) & (x+y)*a = Av.(x*a,y*a) by A7;
hence a*(x+y) = a*x + a*y & (x+y)*a = x*a + y*a by A6;
end;
end;
hence thesis by A1,A3,A4,A5,DefSubRing;
end;
registration let V be Ring;
cluster strict 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 &
1.V = 1.V & 0.V = 0.V by FUNCT_2:40;
then doubleLoopStr (# the carrier of V, the addF of V,
the multF of V, 1.V, 0.V #) is Subring of V by Th01;
hence thesis;
end;
end;
definition
let V be non empty multLoopStr_0;
let V1 be Subset of V;
attr V1 is multiplicatively-closed means :Rdef200:
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 :Rdef211:
(the addF of V)||V1;
correctness
proof
A3:dom(the addF of V) = [:the carrier of V,the carrier of V:]
by FUNCT_2:def 1; then
A4:dom((the addF of V)||V1) =[:V1,V1:] by ZFMISC_1:119,RELAT_1:91;
for z be set st z in [:V1,V1:] holds ((the addF of V)||V1).z in V1
proof
let z be set;
assume A5: z in [:V1,V1:]; then
consider r,x be set such that
A6: r in V1 & x in V1 & z=[r,x] by ZFMISC_1:def 2;
reconsider y=x,r1=r as Element of V by A6;
[r,x] in dom((the addF of V)||V1) by A3,A5,A6,ZFMISC_1:119,RELAT_1:91; then
((the addF of V)||V1).z = r1+y by A6,FUNCT_1:70;
hence ((the addF of V)||V1).z in V1 by A6,A1,IDEAL_1:def 1;
end;
hence thesis by A4,FUNCT_2:5;
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 :Rdef220:
(the multF of V)||V1;
correctness
proof
A3:dom(the multF of V) = [:the carrier of V,the carrier of V:]
by FUNCT_2:def 1; then
A4:dom((the multF of V)||V1) =[:V1,V1:] by ZFMISC_1:119,RELAT_1:91;
for z be set st z in [:V1,V1:] holds ((the multF of V)||V1).z in V1
proof
let z be set;
assume A5: z in [:V1,V1:]; then
consider r,x be set such that
A6: r in V1 & x in V1 & z=[r,x] by ZFMISC_1:def 2;
reconsider y=x,r1=r as Element of V by A6;
[r,x] in dom((the multF of V)||V1) by ZFMISC_1:119,A3,A5,A6,RELAT_1:91;
then ((the multF of V)||V1).z = r1*y by A6,FUNCT_1:70;
hence ((the multF of V)||V1).z in V1 by A1,A6,Rdef200;
end;
hence thesis by A4,FUNCT_2:5;
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 :Rdef213:
0.V;
correctness
proof
consider x be Element of V1;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
P2:-x1 in V1 by A1,Rdef210b;
x1 + -x1 = 0.V by RLVECT_1:def 11;
hence thesis by P2,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 :Rdef214:
1.V;
correctness by A1,Rdef200;
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: V1 is add-closed & V1 is having-inverse by Rdef210; then
Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 &
One_(V1,V) =1_V & mult_(V1,V) = (the multF of V) || V1
by A1,Rdef211,Rdef213,Rdef214,Rdef220;
hence thesis by A1,A2,Th01;
end;
begin :: Some properties of Algebras
reserve V for Algebra;
reserve V1 for Subset of V;
reserve v,w for Element of V;
reserve v1,w1 for Element of V1;
reserve MR for Function of [:REAL,X:],X;
reserve a,b for Real;
definition let V be Algebra;
mode Subalgebra of V -> Algebra means :DefSubAlg:
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 FUNCT_2:40;
end;
end;
theorem Th02:
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
B2: d2 = 1.V and
A3: A = (the addF of V)||V1 and
B3: M = (the multF of V)||V1 and
A4: MR = (the Mult of V) | [:REAL,V1:] and
B4: 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
by STRUCT_0:def 1;
A5:0.W = 0.V & 1.W= 1.V by A2,B2;
A6:now let x,y be Element of W;
x + y = (the addF of V).[x,y] by A1,A3,FUNCT_1:72;
hence x + y = (the addF of V).(x,y);
end;
A7:now let a;
let x be VECTOR of W;
a * x = (the Mult of V).([a,x]) by A1,A4,FUNCT_1:72;
hence a * x = (the Mult of V).(a,x);
end;
B7:now let a,x be VECTOR of W;
a * x = (the multF of V).([a,x]) by A1,B3,FUNCT_1:72;
hence a * x = (the multF of V).(a,x);
end;
W is Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive Algebra-like
proof
set Av = the addF of V; set MV = the Mult of V;
set Mv = the multF 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 A6;
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.(x + y,z1) & x + (y + z) = Av.(x1,y + z) by A6; then
(x + y) + z = (x1 + y1) + z1 & x + (y + z) = x1 + (y1 + z1) by A6;
hence (x + y) + z = x + (y + z) by RLVECT_1:def 6;
end;
hereby let x be VECTOR of W;
reconsider y = x, z = 0.W as VECTOR of V by A1,TARSKI:def 3;
thus x + 0.W = y + 0.V by A2,A6 .= x by RLVECT_1:10;
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
A8: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A8,VECTSP_1:63; then
reconsider y = v as Element of W by A1,B4;
take y;
thus x + y = 0.W by A2,A6,A8;
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 B7;
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 = a1 * b1 & a * (b * x) = Mv.(a,b * x) by B7; then
(a * b) * x = (a1 * b1) * y & a * (b * x) = a1 * (b1 * y) by B7;
hence (a * b) * x = a * (b * x) by GROUP_1:def 4;
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 B7,B2;
hence v * 1.W = v by VECTSP_1:def 13;
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;
T2: x*y = x1*y1 & x*z = x1*z1 by B7;
y+z = y1+z1 by A6; then
x*(y+z) = x1*(y1+z1) by B7; then
x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 11;
hence x*(y+z) = x*y + x*z by T2,A6;
end;
thus W is Algebra-like
proof
let x,y,z being Element of W;
let a,b be Real;
reconsider x1=x, y1=y as Element of V by A1,TARSKI:def 3;
T0: x+y = x1+y1 by A6;
T4: a*x = a*x1 & a*y = a*y1 & b*x = b*x1 by A7;
x*y = x1*y1 by B7; then
a*(x*y) =a*(x1*y1) by A7; then
a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 20;
hence a*(x*y) = (a*x)*y by T4,B7;
a*(x+y) =a*(x1+y1) by T0,A7; then
a*(x+y) =a*x1 + a*y1 by FUNCSDOM:def 20;
hence a*(x+y) = a*x + a*y by T4,A6;
(a+b)*x = (a+b)*x1 by A7; then
(a+b)*x = a*x1 + b*x1 by FUNCSDOM:def 20;
hence (a+b)*x =a*x + b*x by T4,A6;
(a*b)*x = (a*b)*x1 by A7; then
(a*b)*x = a*(b*x1) by FUNCSDOM:def 20;
hence (a*b)*x = a*(b*x) by A7,T4;
end;
end;
hence thesis by A1,A3,B3,A4,A5,DefSubAlg;
end;
registration let V be Algebra;
cluster strict Subalgebra 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 &
the Mult of V = (the Mult of V) | [:REAL,V1:] &
1_V = 1_V & 0.V = 0.V by FUNCT_2:40;
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 Th02;
hence thesis;
end;
end;
definition let V be Algebra, V1 be Subset of V;
attr V1 is additively-linearly-closed means :def210:
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 Subset of V;
coherence
proof
now let V1 be Subset of V;
assume V1 is additively-linearly-closed; then
V1 is add-closed having-inverse by def210;
hence V1 is additively-closed by Rdef210;
end;
hence thesis;
end;
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 :def212:
(the Mult of V) | [:REAL,V1:];
correctness
proof
A2:[:REAL,V1:] c= [:REAL,the carrier of V:] by ZFMISC_1:118;
A3:dom(the Mult of V) = [:REAL,the carrier of V:] by FUNCT_2:def 1; then
A4:dom((the Mult of V) | [:REAL,V1:]) =[:REAL,V1:] by A2,RELAT_1:91;
for z be set st z in [:REAL,V1:] holds
((the Mult of V) | [:REAL,V1:]).z in V1
proof
let z be set such that
A5: z in [:REAL,V1:];
consider r,x be set such that
A6: r in REAL & x in V1 & z=[r,x] by A5,ZFMISC_1:def 2;
reconsider y=x as VECTOR of V by A6;
reconsider r as Real by A6;
[r,x] in dom((the Mult of V) | [:REAL,V1:]) by A2,A3,A5,A6,RELAT_1:91; then
((the Mult of V) | [:REAL,V1:]).z = r*y by A6,FUNCT_1:70;
hence thesis by A1,A6,def210;
end;
hence thesis by A4,FUNCT_2:5;
end;
end;
definition let V be non empty RLSStruct;
attr V is scalar-mult-cancelable means :DefSMC:
for a be Real, v be Element of V st a*v=0.V holds a=0 or v=0.V;
end;
theorem RLVECT123:
for V being add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr), a be Real holds
a*0.V = 0.V
proof
let V be add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr);
let a be Real;
a * 0.V + a * 0.V = a * (0.V + 0.V) by FUNCSDOM:def 20; then
a * 0.V + a * 0.V = a * 0.V by RLVECT_1:10; then
a * 0.V + a * 0.V = a * 0.V + 0.V by RLVECT_1:10;
hence a * 0.V = 0.V by RLVECT_1:21;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr) st
V is scalar-mult-cancelable holds V is RealLinearSpace
proof
let V being Abelian add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr);
assume A1: V is scalar-mult-cancelable;
B0:1 * 0.V = 0.V by RLVECT123;
A2:for v being VECTOR of V holds 1 * v = v
proof
let v be VECTOR of V;
B1: (1*v) - (1*v) = 0.V by RLVECT_1:28;
(1*v) + (1 * -v) = 1 * (v + -v) by FUNCSDOM:def 20; then
(1*v) + (1 * -v) = 1 * 0.V by RLVECT_1:16; then
B2: -(1*v) = 1*(-v) by B0,B1,RLVECT_1:21;
1 * v = (1 * 1) * v .= 1 * (1 * v) by FUNCSDOM:def 20; then
1 * (1 * v) - 1 * v = 0.V by RLVECT_1:28; then
1 * (1 * v - v) = 0.V by B2,FUNCSDOM:def 20; then
(1*v) - v = 0.V by A1,DefSMC;
hence 1*v = v by RLVECT_1:35;
end;
(for a be Real for v,w being VECTOR of V holds a*(v+w) = a*v + a*w) &
(for a,b be Real for v being VECTOR of V holds (a+b)*v = a*v + b*v) &
(for a,b be Real for v being VECTOR of V holds (a*b)*v = a*(b*v))
by FUNCSDOM:def 20;
hence thesis by A2,RLVECT_1:def 9;
end;
LmAlgebra:
for V being Abelian add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr) st
for v being VECTOR of V holds 1 * v = v holds V is RealLinearSpace
proof
let V being Abelian add-associative right_zeroed right_complementable
Algebra-like (non empty AlgebraStr);
assume A1: for v being VECTOR of V holds 1 * v = v;
(for a be Real for v,w being VECTOR of V holds a*(v+w) = a*v + a*w) &
(for a,b be Real for v being VECTOR of V holds (a+b)*v = a*v + b*v) &
(for a,b be Real for v being VECTOR of V holds (a*b)*v = a*(b*v))
by FUNCSDOM:def 20;
hence thesis by A1,RLVECT_1:def 9;
end;
theorem Th03:
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: V1 is add-closed having-inverse &
for a be Real, v be Element of V st v in V1 holds a*v in V1 by def210; then
Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 &
One_(V1,V) =1_V & mult_(V1,V) = (the multF of V) || V1 &
Mult_(V1,V) = (the Mult of V) | [:REAL,V1:]
by A1,Rdef213,Rdef211,Rdef214,Rdef220,def212;
hence thesis by A1,A2,Th02;
end;
registration let X be non empty set;
cluster RAlgebra X -> Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive Algebra-like;
correctness by FUNCSDOM:50;
end;
theorem LmAlgebra2:
RAlgebra X is RealLinearSpace
proof
for v being VECTOR of RAlgebra X holds 1 * v = v by FUNCSDOM:23;
hence thesis by LmAlgebra;
end;
theorem RLSUB121:
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 AS: x1=x & y1=y;
x1 + y1 = ((the addF of V)||the carrier of V1).[x1,y1] by DefSubAlg;
hence x1 + y1 = x+y by AS,FUNCT_1:72;
end;
hereby let x1,y1 be Element of V1, x,y be Element of V;
assume AS: x1=x & y1=y;
x1 * y1 = ((the multF of V)||the carrier of V1).[x1,y1] by DefSubAlg;
hence x1 * y1 = x*y by AS,FUNCT_1:72;
end;
hereby let v1 be Element of V1, v be Element of V, a be Real;
assume AS: v1 = v;
a * v1 = ((the Mult of V) | [:REAL,the carrier of V1:]).[a,v1]
by DefSubAlg;
hence a * v1 = a * v by AS,FUNCT_1:72;
end;
thus thesis by DefSubAlg;
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 is_bounded_on X };
correctness
proof
P1:{ f where f is Function of X,REAL : f is_bounded_on X } c= Funcs(X,REAL)
proof
let x be set;
assume x in { f where f is Function of X,REAL : f is_bounded_on X }; then
ex f be Function of X,REAL st x=f & f is_bounded_on X;
hence x in Funcs(X,REAL) by FUNCT_2:11;
end;
{ f where f is Function of X,REAL : f is_bounded_on X } is non empty
proof
reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:58;
for x be Element of X st x in X /\ dom g holds g.x =0 by FUNCOP_1:13; then
g is_constant_on X by PARTFUN2:76; then
g is_bounded_on X by RFUNCT_1:108; then
g in { f where f is Function of X,REAL : f is_bounded_on X };
hence thesis;
end;
hence thesis by P1;
end;
end;
theorem ThB7:
BoundedFunctions X is additively-linearly-closed multiplicatively-closed
proof
set W = BoundedFunctions X;
set V = RAlgebra X;
P0:RAlgebra X is RealLinearSpace by LmAlgebra2;
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
XS1: v in W & u in W;
consider v1 be Function of X,REAL such that
L010:v1=v & v1 is_bounded_on X by XS1;
consider u1 be Function of X,REAL such that
L020:u1=u & u1 is_bounded_on X by XS1;
dom(v1+u1) = X /\ X by FUNCT_2:def 1; then
L04:v1+u1 is Function of X,REAL & v1+u1 is_bounded_on X
by L010,L020,RFUNCT_1:100;
reconsider h = v+u as Element of Funcs(X,REAL);
XSF:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1; then
R3: dom v1 /\ dom u1 = X /\ X by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = v1.x + u1.x
by L010,L020,FUNCSDOM:10; then
v+u=v1+u1 by VALUED_1:def 1,R3,XSF;
hence v+u in W by L04;
end; then
P1:W is add-closed by IDEAL_1:def 1;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V such that
XS1: v in W;
consider v1 be Function of X,REAL such that
L010:v1=v & v1 is_bounded_on X by XS1;
M1: -v1 is Function of X,REAL & -v1 is_bounded_on X
by L010,RFUNCT_1:99;
reconsider h = -v, v2 = v as Element of Funcs(X,REAL);
R1: h=(-1)*v by P0,RLVECT_1:29;
XSF:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
R3: dom v1 =X by FUNCT_2:def 1;
now let x be set;
assume x in dom h; then
reconsider y=x as Element of X;
h.x = (-1)*(v2.y) by R1,FUNCSDOM:15;
hence h.x = -v1.x by L010;
end; then
-v=-v1 by VALUED_1:9,R3,XSF;
hence -v in W by M1;
end; then
Q1:W is having-inverse by Rdef210b;
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 such that
XS1: u in W;
consider u1 be Function of X,REAL such that
L110:u1=u & u1 is_bounded_on X by XS1;
M2: a(#)u1 is Function of X,REAL & a(#)u1 is_bounded_on X
by L110,RFUNCT_1:97;
reconsider h = a*u as Element of Funcs(X,REAL);
XSF:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
R3: dom u1 = X by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = a*(u1.x) by L110,FUNCSDOM:15; then
a*u=a(#)u1 by VALUED_1:def 5,R3,XSF;
hence a*u in W by M2;
end;
hence BoundedFunctions X is additively-linearly-closed by P1,Q1,def210;
Q2: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
XS1: v in W & u in W;
consider v1 be Function of X,REAL such that
L010:v1=v & v1 is_bounded_on X by XS1;
consider u1 be Function of X,REAL such that
L020:u1=u & u1 is_bounded_on X by XS1;
dom(v1(#)u1) = X /\ X by FUNCT_2:def 1; then
M3: v1(#)u1 is Function of X,REAL & v1(#)u1 is_bounded_on X
by L010,L020,RFUNCT_1:101;
reconsider h = v*u as Element of Funcs(X,REAL);
XSF:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1; then
R3: dom v1 /\ dom u1 = X /\ X by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = v1.x *u1.x
by L010,L020,FUNCSDOM:11; then
v*u=v1(#)u1 by VALUED_1:def 4,R3,XSF;
hence v*u in W by M3;
end;
reconsider g = RealFuncUnit X as Function of X,REAL;
for x be Element of X st x in X /\ dom g holds g.x =1 by FUNCOP_1:13; then
g is_constant_on X by PARTFUN2:76; then
g is_bounded_on X by RFUNCT_1:108; then
1.V in W;
hence thesis by Rdef200,Q2;
end;
registration let X;
cluster BoundedFunctions X -> additively-linearly-closed
multiplicatively-closed;
coherence by ThB7;
end;
theorem
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
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 Th03;
end;
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 Th03; then
1 * v = 1*v1 by RLSUB121;
hence 1 * v =v by FUNCSDOM:23;
end;
hence thesis by LmAlgebra;
end;
reserve F,G,H for VECTOR of R_Algebra_of_BoundedFunctions X;
reserve f,g,h for Function of X,REAL;
theorem ThB10:
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;
A4:R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume A6: H = F+G;
let x be Element of X;
h1=f1+g1 by A4,A6,RLSUB121;
hence h.x = f.x+g.x by A1,FUNCSDOM:10;
end;
assume for x be Element of X holds h.x = f.x+g.x; then
h1=f1+g1 by A1,FUNCSDOM:10;
hence H =F+G by A4,RLSUB121;
end;
theorem ThB11:
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;
A3:R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
reconsider f1=F, g1=G as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume A5: G = a*F;
let x be Element of X;
g1=a*f1 by A3,A5,RLSUB121;
hence g.x=a*f.x by A1,FUNCSDOM:15;
end;
assume for x be Element of X holds g.x=a*f.x; then
g1=a*f1 by A1,FUNCSDOM:15;
hence G =a*F by A3,RLSUB121;
end;
theorem ThB12:
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:R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume A3: H = F*G;
let x be Element of X;
h1 = f1*g1 by A2,A3,RLSUB121;
hence h.x = f.x * g.x by A1,FUNCSDOM:11;
end;
assume for x be Element of X holds h.x = f.x * g.x; then
h1 = f1 * g1 by A1,FUNCSDOM:11;
hence H = F * G by A2,RLSUB121;
end;
theorem ThB12Zero:
0.R_Algebra_of_BoundedFunctions X = X -->0
proof
A1:R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
0.RAlgebra X = X -->0;
hence thesis by A1,RLSUB121;
end;
theorem ThB12One:
1_R_Algebra_of_BoundedFunctions X = X -->1
proof
A1:R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th03;
1_RAlgebra X = X -->1;
hence thesis by A1,RLSUB121;
end;
definition let X be non empty set, F be set such that
A1:F in BoundedFunctions X;
func modetrans(F,X) -> Function of X,REAL means :DefB7:
it=F & it is_bounded_on X;
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
{ abs(f.x) where x is Element of X : not contradiction };
coherence
proof
A1:now let z be set;
now assume z in {abs(f.x) where x is Element of X : not contradiction };
then
ex x be Element of X st z=abs(f.x);
hence z in REAL;
end;
hence z in {abs(f.x) where x is Element of X : not contradiction }
implies z in REAL;
end;
consider z be Element of X;
abs(f.z) in {abs(f.x) where x is Element of X : not contradiction };
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem ThB13:
f is_bounded_on X implies PreNorms f is non empty bounded_above
proof
assume f is_bounded_on X; then
consider K be real number such that
A1: for x be set st x in X /\ dom f holds abs(f.x) <= K by RFUNCT_1:90;
A3:X /\ dom f = X /\ X by FUNCT_2:def 1;
now let r be real number;
assume r in PreNorms f; then
ex t be Element of X st r=abs(f.t);
hence r <=K by A1,A3;
end;
hence PreNorms f is non empty bounded_above by SEQ_4:def 1;
end;
theorem
f is_bounded_on X iff PreNorms f is bounded_above
proof
now assume A1: PreNorms f is bounded_above;
reconsider K = sup PreNorms f as Real;
A7: now let t be set;
assume t in X /\ dom f; then
abs(f.t) in PreNorms f;
hence abs(f.t) <= K by A1,SEQ_4:def 4;
end;
take K;
thus f is_bounded_on X by A7,RFUNCT_1:90;
end;
hence thesis by ThB13;
end;
theorem ThB15:
ex NORM be Function of BoundedFunctions X,REAL st
for F be set st F in BoundedFunctions X holds
NORM.F = sup PreNorms(modetrans(F,X))
proof
deffunc F(set) = sup PreNorms(modetrans($1,X));
A1:for z be set st z in BoundedFunctions X holds F(z) in REAL;
ex f being Function of BoundedFunctions X,REAL st
for x being set st x in BoundedFunctions X holds
f.x = F(x) from FUNCT_2:sch 2(A1);
hence thesis;
end;
definition let X be non empty set;
func BoundedFunctionsNorm X -> Function of BoundedFunctions X,REAL means:DefB9:
for x be set st x in BoundedFunctions X holds
it.x = sup PreNorms(modetrans(x,X));
existence by ThB15;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedFunctions X,REAL such that
A1: for x be set st x in BoundedFunctions X holds
NORM1.x = sup PreNorms(modetrans(x,X)) and
A2: for x be set st x in BoundedFunctions X holds
NORM2.x = sup PreNorms(modetrans(x,X));
A3:dom NORM1 = BoundedFunctions X &
dom NORM2 = BoundedFunctions X by FUNCT_2:def 1;
for z be set st z in BoundedFunctions X holds NORM1.z = NORM2.z
proof
let z be set such that
A4: z in BoundedFunctions X;
NORM1.z = sup PreNorms(modetrans(z,X)) by A1,A4;
hence thesis by A2,A4;
end;
hence thesis by A3,FUNCT_1:9;
end;
end;
theorem ThB16:
f is_bounded_on X implies modetrans(f,X) = f
proof
assume f is_bounded_on X; then
f in BoundedFunctions X;
hence thesis by DefB7;
end;
theorem ThB17:
f is_bounded_on X implies (BoundedFunctionsNorm X).f = sup PreNorms f
proof
reconsider f'=f as set;
assume A0:f is_bounded_on X; then
f in BoundedFunctions X; then
(BoundedFunctionsNorm X).f = sup PreNorms(modetrans(f',X)) by DefB9;
hence (BoundedFunctionsNorm X).f = sup PreNorms f by ThB16,A0;
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
proof
thus the carrier of R_Normed_Algebra_of_BoundedFunctions X is non empty;
thus thesis;
end;
end;
UNITAL:
now let X be non empty set;
set F = R_Normed_Algebra_of_BoundedFunctions X;
let x,e be Element of F;
assume
A1: e = One_(BoundedFunctions X,RAlgebra X);
set X1 = BoundedFunctions X;
reconsider f = x as Element of X1;
1_RAlgebra X = 1_R_Algebra_of_BoundedFunctions X by ThB12One; then
P5:[f,1_RAlgebra X] in [:X1,X1:] & [1_RAlgebra X,f] in [:X1,X1:]
by ZFMISC_1:106;
x * e = (mult_(X1,RAlgebra X)).(f,1_RAlgebra X) by A1,Rdef214; then
x * e = ((the multF of RAlgebra X)||X1).(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;
e * x = (mult_(X1,RAlgebra X)).(1_RAlgebra X,f) by A1,Rdef214; then
e * x = ((the multF of RAlgebra X)||X1).(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;
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 UNITAL;
end;
end;
theorem RSSPACE34:
for W be Normed_AlgebraStr, V be Algebra st
the AlgebraStr of W = V & 1.V = 1.W holds W is Algebra
proof
let W be Normed_AlgebraStr,V be Algebra such that
A1:the AlgebraStr of W = V & 1.V =1.W;
reconsider W as non empty AlgebraStr by A1,STRUCT_0:def 1;
L1: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 x + y = y + x by A1;
end;
L2: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 6;
hence (x + y) + z = x + (y + z) by A1;
end;
L3:for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x, z = 0.W as VECTOR of V by A1;
x + 0.W = y + 0.V by A1;
hence x + 0.W = x by RLVECT_1:10;
end;
L4: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
A8: x1 + v = 0.V by ALGSTR_0:def 11;
reconsider y = v as Element of W by A1;
x + y = 0.W by A8,A1;
hence thesis by ALGSTR_0:def 11;
end;
L5: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 v * w =w*v by A1;
end;
L6: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 4;
hence (a * b) * x = a * (b * x) by A1;
end;
L7: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 x*1.W = x by VECTSP_1:def 13;
end;
L8: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 11;
hence x*(y+z) = x*y + x*z by A1;
end;
W is Algebra-like
proof
let x,y,z being Element of W;
let a,b be Real;
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
a*(x*y) = a*(x1*y1) by A1; then
a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 20;
hence a*(x*y) = (a*x)*y by A1;
a*(x+y) = a*(x1+y1) by A1; then
a*(x+y) = a*x1 + a*y1 by FUNCSDOM:def 20;
hence a*(x+y) = a*x + a*y by A1;
(a+b)*x = (a+b)*x1 by A1; then
(a+b)*x = a*x1 + b*x1 by FUNCSDOM:def 20;
hence (a+b)*x =a*x + b*x by A1;
(a*b)*x = (a*b)*x1 by A1; then
(a*b)*x = a*(b*x1) by FUNCSDOM:def 20;
hence (a*b)*x = a*(b*x) by A1;
end;
hence thesis by L1,L2,L3,L4,L5,L6,L7,L8,RLVECT_1:def 5,def 6,def 7,
ALGSTR_0:def 16,GROUP_1:def 4,def 16;
end;
reserve F,G,H for Point of R_Normed_Algebra_of_BoundedFunctions X;
theorem LmAlgebra4:
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 RSSPACE34;
end;
theorem FUNCSDOM23:
(Mult_(BoundedFunctions X,RAlgebra X)).(1,F) = F
proof
set X1 = BoundedFunctions X;
reconsider f1 = F as Element of X1;
A2:[1,f1] in [:REAL,X1:] by ZFMISC_1:106;
thus (Mult_(BoundedFunctions X,RAlgebra X)).(1,F)
= ((the Mult of RAlgebra X)| [:REAL,X1:]).(1,f1) by def212
.= (the Mult of RAlgebra X).(1,f1) by A2,FUNCT_1:72
.= F by FUNCSDOM:23;
end;
theorem LmAlgebra5:
R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
P1:for v being VECTOR of R_Normed_Algebra_of_BoundedFunctions X
holds 1 * v = v by FUNCSDOM23;
R_Normed_Algebra_of_BoundedFunctions X is Algebra by LmAlgebra4;
hence thesis by LmAlgebra,P1;
end;
theorem ThB18:
X-->0 = 0.R_Normed_Algebra_of_BoundedFunctions X
proof
X-->0 = 0.R_Algebra_of_BoundedFunctionsX by ThB12Zero;
hence X-->0 =0.R_Normed_Algebra_of_BoundedFunctions X;
end;
theorem ThB19:
f=F & f is_bounded_on X implies abs(f.x) <= ||.F.||
proof
assume A1: f=F & f is_bounded_on X; then
A2:PreNorms f is non empty bounded_above by ThB13;
abs(f.x) in PreNorms f; then
abs(f.x) <= sup PreNorms f by A2,SEQ_4:def 4;
hence abs(f.x) <= ||.F.|| by A1,ThB17;
end;
theorem
0 <= ||.F.||
proof
F in BoundedFunctions X; then
consider g be Function of X,REAL such that
A0: F=g & g is_bounded_on X;
A1:now let r be Real;
assume r in PreNorms g; then
ex t be Element of X st r=abs(g.t);
hence 0 <= r by COMPLEX1:132;
end;
A4:PreNorms g is non empty bounded_above by A0,ThB13;
consider r0 be set such that
A5: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A5;
0 <= r0 by A1,A5; then
0 <=sup PreNorms g by A4,A5,SEQ_4:def 4;
hence thesis by A0,ThB17;
end;
theorem ThB21:
F = 0.R_Normed_Algebra_of_BoundedFunctions X implies 0 = ||.F.||
proof
assume A1: F = 0.R_Normed_Algebra_of_BoundedFunctions X;
set z = X --> 0;
reconsider z as Function of X, REAL by FUNCOP_1:58;
F in BoundedFunctions X; then
consider g be Function of X,REAL such that
A0: g=F & g is_bounded_on X;
A3: now let r be Real;
assume r in PreNorms g; then
consider t be Element of X such that
A5: r=abs(g.t);
z=g by A1,A0,ThB18; then
abs(g.t) = abs(0) by FUNCOP_1:13;
hence 0 <= r & r <=0 by A5,ABSVALUE:7;
end;
A6: PreNorms g is non empty bounded_above by A0,ThB13;
consider r0 be set such that
A7: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A7;
A8: 0 <= r0 & r0<=0 by A3,A7;
(for s be real number st s in PreNorms g holds s <= 0)
implies sup PreNorms g <= 0 by SEQ_4:62; then
sup PreNorms g = 0 by A3,A6,A7,A8,SEQ_4:def 4;
hence thesis by A0,ThB17;
end;
theorem ThB22:
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 R_Algebra_of_BoundedFunctions X;
H=F+G iff h1=f1+g1;
hence thesis by A1,ThB10;
end;
theorem ThB23:
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 R_Algebra_of_BoundedFunctions X;
G=a*F iff g1=a*f1;
hence thesis by A1,ThB11;
end;
theorem ThB23a:
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 R_Algebra_of_BoundedFunctions X;
H=F*G iff h1=f1*g1;
hence thesis by A1,ThB12;
end;
theorem ThB24:
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_BoundedFunctions X ) &
||.a*F.|| = abs a * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
A1:now assume A2: ||.F.|| = 0;
F in BoundedFunctions X; then
consider g be Function of X,REAL such that
A3: F=g & g is_bounded_on X;
set z = X --> 0;
reconsider z as Function of X,REAL by FUNCOP_1:58;
now let t be Element of X;
abs(g.t) <= ||.F.|| by A3,ThB19; then
abs(g.t) = 0 by A2,COMPLEX1:132;
hence g.t =0 by ABSVALUE:7 .=z.t by FUNCOP_1:13;
end; then
g=z by FUNCT_2:113;
hence F=0.R_Normed_Algebra_of_BoundedFunctions X by A3,ThB18;
end;
A3:now assume A4: F = 0.R_Normed_Algebra_of_BoundedFunctions X;
set z = X --> 0;
reconsider z as Function of X,REAL by FUNCOP_1:58;
F in BoundedFunctions X; then
consider g be Function of X,REAL such that
A41: F=g & g is_bounded_on X;
A5: z=g by A41,A4,ThB18;
A6: now let r be Real such that
A7: r in PreNorms g;
consider t be Element of X such that
A8: r=abs(g.t) by A7;
abs(g.t) = abs(0) by A5,FUNCOP_1:13 .= 0 by ABSVALUE:7;
hence 0 <= r & r <=0 by A8;
end;
A9: PreNorms g is non empty bounded_above by A41,ThB13;
consider r0 be set such that
A10: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A10;
A11:0<=r0 by A6,A10;
(for s be real number st s in PreNorms g holds s <= 0)
implies sup PreNorms g <= 0 by SEQ_4:62; then
sup PreNorms g = 0 by A6,A9,A10,A11,SEQ_4:def 4;
hence ||.F.|| = 0 by A41,ThB17;
end;
A12:||.a*F.|| = abs a * ||.F.||
proof
F in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
A121:f1=F & f1 is_bounded_on X;
a*F in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A122:h1=a*F & h1 is_bounded_on X;
A13:now let t be Element of X;
abs(h1.t) = abs(a*f1.t) by A121,A122,ThB23; then
A15: abs(h1.t) = abs a * abs(f1.t) by COMPLEX1:151;
0<= abs a by COMPLEX1:132;
hence abs(h1.t) <= abs a *||.F.|| by A15,A121,ThB19,XREAL_1:66;
end;
A17:now let r be Real;
assume r in PreNorms h1; then
ex t be Element of X st r=abs(h1.t);
hence r <= abs a *||.F.|| by A13;
end;
(for s be real number st s in PreNorms h1 holds s <= abs a *||.F.|| )
implies sup PreNorms h1 <= abs a *||.F.|| by SEQ_4:62; then
A21:||.a*F.|| <= abs a *||.F.|| by A17,A122,ThB17;
per cases;
suppose A22: a <> 0; then
A31: abs(a) <>0 by COMPLEX1:133;
A23: now let t be Element of X;
h1.t=a*f1.t by A121,A122,ThB23; then
a"*h1.t = (a"* a)*f1.t; then
A24: a"*h1.t =1*f1.t by A22,XCMPLX_0:def 7;
A25: abs(a"*h1.t) = abs(a")*abs(h1.t) by COMPLEX1:151;
A27: 0 <= abs(a") by COMPLEX1:132;
abs(a") =abs(1/a); then
abs(a") =1/abs(a) by ABSVALUE:15;
hence abs(f1.t) <= abs(a)"*||.a*F.||
by A24,A25,A122,ThB19,A27,XREAL_1:66;
end;
A28: now let r be Real;
assume r in PreNorms f1; then
ex t be Element of X st r=abs(f1.t);
hence r <= abs(a)"*||.a*F.|| by A23;
end;
A32: (for s be real number st s in PreNorms f1 holds s <= abs(a)"*||.a*F.||)
implies sup PreNorms f1 <= abs(a)"*||.a*F.|| by SEQ_4:62;
A33: ||.F.|| <=abs(a)"*||.a*F.|| by A28,A32,A121,ThB17;
0 <= abs a by COMPLEX1:132; then
abs(a)*||.F.|| <=abs(a)*(abs(a)"*||.a*F.||) by A33,XREAL_1:66; then
abs(a)*||.F.|| <=(abs(a)*abs(a)")*||.a*F.||; then
abs(a)*||.F.|| <=1*||.a*F.|| by A31,XCMPLX_0:def 7;
hence ||.a*F.|| = abs(a) * ||.F.|| by A21,XXREAL_0:1;
end;
suppose A34: a=0;
reconsider fz=F as VECTOR of R_Algebra_of_BoundedFunctions X;
a*fz =(a+a)*fz by A34 .=a*fz + a* fz by FUNCSDOM:def 20; then
0.R_Algebra_of_BoundedFunctions X
= -(a*fz)+(a*fz + a* fz) by VECTSP_1:63; then
0.R_Algebra_of_BoundedFunctions X
= -(a*fz)+a*fz + a* fz by RLVECT_1:def 6; then
0.R_Algebra_of_BoundedFunctions X
= 0.R_Algebra_of_BoundedFunctions X + a * fz by VECTSP_1:63; then
A35: a*F =0.R_Normed_Algebra_of_BoundedFunctions X by RLVECT_1:10;
abs(a)* ||.F.|| =0 * ||.F.|| by A34,ABSVALUE:7;
hence abs(a)* ||.F.|| =||.a*F.|| by A35,ThB21;
end;
end;
||.F+G.|| <= ||.F.|| + ||.G.||
proof
F in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
A361:f1=F & f1 is_bounded_on X;
G in BoundedFunctions X; then
consider g1 be Function of X,REAL such that
A362:g1=G & g1 is_bounded_on X;
F+G in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A363:h1=F+G & h1 is_bounded_on X;
A36:now let t be Element of X;
A37: abs(h1.t) =abs(f1.t+g1.t) by A361,A362,A363,ThB22;
A38: abs(f1.t+g1.t) <=abs(f1.t) +abs(g1.t) by COMPLEX1:142;
abs(f1.t) <= ||.F.|| & abs(g1.t)<= ||.G.|| by A361,A362,ThB19; then
abs(f1.t) +abs(g1.t) <= ||.F.|| + ||.G.|| by XREAL_1:9;
hence abs(h1.t) <= ||.F.|| + ||.G.|| by A37,A38,XXREAL_0:2;
end;
A40:now let r be Real;
assume r in PreNorms h1; then
ex t be Element of X st r=abs(h1.t);
hence r <= ||.F.|| + ||.G.|| by A36;
end;
(for s be real number st s in PreNorms h1 holds s <= ||.F.|| + ||.G.||)
implies sup PreNorms h1 <= ||.F.|| + ||.G.|| by SEQ_4:62;
hence ||.F+G.|| <=||.F.|| + ||.G.|| by A40,A363,ThB17;
end;
hence thesis by A1,A3,A12;
end;
theorem ThB25:
R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like
proof
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.|| = abs(a) * ||.x.|| &
||.x+y.|| <= ||.x.|| + ||.y.|| by ThB24;
hence thesis by NORMSP_1:def 2;
end;
registration let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X ->
RealNormSpace-like RealLinearSpace-like
Abelian add-associative right_zeroed right_complementable;
coherence by ThB25,LmAlgebra5;
end;
theorem ThB27:
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;
A4:now assume H=F-G; then
H+G=F-(G-G) by RLVECT_1:43; then
H+G=F-0.R_Normed_Algebra_of_BoundedFunctions X by RLVECT_1:28; then
A5: H+G=F by RLVECT_1:26;
now let x be Element of X;
f.x=h.x + g.x by A1,A5,ThB22;
hence f.x-g.x=h.x;
end;
hence for x be Element of X holds h.x = f.x - g.x;
end;
now assume
A6: 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 A6;
hence h.x + g.x= f.x;
end; then
F=H+G by A1,ThB22; then
F-G=H+(G-G) by RLVECT_1:def 6; then
F-G=H+0.R_Normed_Algebra_of_BoundedFunctions X by RLVECT_1:28;
hence F-G=H by RLVECT_1:10;
end;
hence thesis by A4;
end;
theorem ThB28:
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;
assume A2: vseq is Cauchy_sequence_by_Norm;
now let e1 be real number such that
A4: e1 >0;
reconsider e =e1 as Real by XREAL_0:def 1;
consider k be Element of NAT such that
A5: for n,m be Element of NAT st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A2,A4,RSSPACE3:10;
A6: now let m be Element of NAT;
assume m >= k; then
A7: ||. vseq.m - vseq.k .|| = k holds
abs(||.vseq.||.m - ||.vseq.||.k ) < e1 by A6;
end; then
A3:||.vseq.|| is convergent by SEQ_4:58;
defpred P[set,set] means
ex xseq be Real_Sequence st
(for n be Element of NAT holds xseq.n=modetrans(vseq.n,X).$1) &
xseq is convergent & $2= lim xseq;
A11: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(Element of NAT) = modetrans(vseq.$1,X).x;
consider xseq be Real_Sequence such that
A12: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4;
A13:for m,k be Element of NAT holds abs(xseq.m-xseq.k) <= ||.vseq.m - vseq.k.||
proof
let m,k be Element of NAT;
vseq.m in BoundedFunctions X; then
ex vseqm be Function of X,REAL st
vseq.m=vseqm & vseqm is_bounded_on X; then
A14: modetrans(vseq.m,X)=vseq.m by ThB16;
vseq.k in BoundedFunctions X; then
ex vseqk be Function of X,REAL st
vseq.k=vseqk & vseqk is_bounded_on X; then
A15: modetrans(vseq.k,X)=vseq.k by ThB16;
vseq.m-vseq.k in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A161: h1=vseq.m-vseq.k & h1 is_bounded_on X;
xseq.m =modetrans(vseq.m,X).x & xseq.k =modetrans(vseq.k,X).x by A12; then
xseq.m - xseq.k = h1.x by A14,A15,A161,ThB27;
hence thesis by ThB19,A161;
end;
now let e be real number such that
A18: e > 0;
e is Real by XREAL_0:def 1; then
consider k be Element of NAT such that
A19: for n, m be Element of NAT st n >= k & m >= k holds
||.(vseq.n) - (vseq.m).|| < e by A2,A18,RSSPACE3:10;
take k;
hereby let n be Element of NAT;
assume n >=k; then
A21: ||. vseq.n - vseq.k .|| < e by A19;
abs(xseq.n-xseq.k) <= ||. vseq.n - vseq.k .|| by A13;
hence abs(xseq.n-xseq.k) < e by A21,XXREAL_0:2;
end;
end; then
A17:xseq is convergent by SEQ_4:58;
take y = lim xseq;
thus thesis by A12,A17;
end;
consider tseq be Function of X,REAL such that
A22:for x be Element of X holds P[x,tseq.x] from FUNCT_2:sch 3(A11);
now let x be set;
assume AD0: x in X /\ dom tseq; then
consider xseq be Real_Sequence such that
A25: (for n be Element of NAT holds xseq.n=modetrans(vseq.n,X).x) &
xseq is convergent & tseq.x = lim xseq by A22;
A28:abs xseq is convergent & abs(tseq.x) = lim abs(xseq) by A25,SEQ_4:26,27;
for n be Element of NAT holds abs(xseq).n <= ||.vseq.|| .n
proof
let n be Element of NAT;
vseq.n in BoundedFunctions X; then
A261:ex h1 be Function of X,REAL st vseq.n=h1 & h1 is_bounded_on X; then
A27: modetrans(vseq.n,X)=vseq.n by ThB16;
xseq.n =modetrans(vseq.n,X).x by A25; then
abs(xseq.n) <= ||.vseq.n.|| by A27,A261,AD0,ThB19; then
abs(xseq).n <= ||.vseq.n.|| by VALUED_1:18;
hence abs(xseq).n <= ||.vseq.|| .n by NORMSP_1:def 10;
end;
hence abs(tseq.x) <= lim ||.vseq.|| by A3,A28,SEQ_2:32;
end; then
A23:tseq is_bounded_on X by RFUNCT_1:90;
A31:
for e be Real st e > 0
ex k be Element of NAT st
for n be Element of NAT st n >= k holds
for x be Element of X holds abs(modetrans(vseq.n,X).x - tseq.x) <= e
proof
let e be Real such that
A32: e > 0;
consider k be Element of NAT such that
A33: for n,m be Element of NAT st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A2,A32,RSSPACE3:10;
A34:now let n be Element of NAT such that
A35: n >= k;
now let x be Element of X;
consider xseq be Real_Sequence such that
A36: (for n be Element of NAT holds xseq.n=modetrans(vseq.n,X).x) &
xseq is convergent & tseq.x = lim xseq by A22;
A37: for m,k be Element of NAT holds
abs(xseq.m-xseq.k) <= ||.vseq.m - vseq.k.||
proof
let m,k be Element of NAT;
vseq.m in BoundedFunctions X; then
ex vseqm be Function of X,REAL st
vseq.m=vseqm & vseqm is_bounded_on X; then
A38: modetrans(vseq.m,X) = vseq.m by ThB16;
vseq.k in BoundedFunctions X; then
ex vseqk be Function of X,REAL st
vseq.k=vseqk & vseqk is_bounded_on X; then
A39: modetrans(vseq.k,X)=vseq.k by ThB16;
vseq.m-vseq.k in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A401: h1 =vseq.m-vseq.k & h1 is_bounded_on X;
A40: xseq.m =modetrans(vseq.m,X).x by A36;
xseq.k =modetrans((vseq.k),X).x by A36; then
xseq.m - xseq.k =h1.x by A38,A39,A40,A401,ThB27;
hence abs(xseq.m-xseq.k) <= ||.vseq.m - vseq.k.|| by ThB19,A401;
end;
deffunc G0(Element of NAT) = xseq.n;
consider fseq be Real_Sequence such that
A42: for m be Element of NAT holds fseq.m = G0(m) from SEQ_1:sch 1;
A42a: fseq is constant by SEQM_3:def 6,A42; then
A42b: fseq is convergent by SEQ_4:39;
lim fseq = fseq.0 by A42a,SEQ_4:41; then
A42c: lim fseq =xseq.n by A42;
set wseq = xseq-fseq;
A43: now let m be Element of NAT;
wseq.m = xseq.m +(-fseq).m by SEQ_1:11; then
wseq.m = xseq.m +-fseq.m by SEQ_1:14;
hence wseq.m = xseq.m - xseq.n by A42;
end;
deffunc F(Element of NAT) = abs(xseq.$1 - xseq.n);
consider rseq be Real_Sequence such that
A44: for m be Element of NAT holds rseq.m = F(m) from SEQ_1:sch 1;
A46: wseq is convergent by A36,A42b,SEQ_2:25;
A47: lim wseq= tseq.x - xseq.n by A36,A42b,A42c,SEQ_2:26;
now let x be set such that
A48: x in NAT;
reconsider k=x as Element of NAT by A48;
rseq.x = abs(xseq.k - xseq.n) by A44; then
rseq.x = abs(wseq.k) by A43;
hence rseq.x = abs(wseq).x by VALUED_1:18;
end; then
rseq = abs(wseq) by SEQ_1:8; then
A45: rseq is convergent & lim rseq = abs(tseq.x-xseq.n)
by A46,A47,SEQ_4:26,SEQ_4:27;
for m be Element of NAT st m >= k holds rseq.m <= e
proof
let m be Element of NAT such that
A49: m >=k;
rseq.m = abs(xseq.m-xseq.n) by A44; then
rseq.m = abs(xseq.n-xseq.m) by COMPLEX1:146; then
A41: rseq.m <= ||.vseq.n - vseq.m.|| by A37;
||.vseq.n - vseq.m.|| 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 such that
A51: e > 0;
consider k be Element of NAT such that
A52: for n be Element of NAT st n >= k holds
for x be Element of X holds
abs(modetrans((vseq.n),X).x - tseq.x) <= e by A31,A51;
take k;
hereby let n be Element of NAT such that
A53: n >= k;
vseq.n in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
G1: f1=vseq.n & f1 is_bounded_on X;
vseq.n-tv in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A531: h1=vseq.n-tv & h1 is_bounded_on X;
A54: now let t be Element of X;
J1: modetrans(vseq.n,X)=f1 by G1,DefB7;
h1.t = f1.t- tseq.t by G1,A531,ThB27;
hence abs(h1.t) <=e by A52,A53,J1;
end;
A55: now let r be Real;
assume r in PreNorms h1; then
ex t be Element of X st r=abs(h1.t);
hence r <=e by A54;
end;
(for s be real number st s in PreNorms h1 holds s <= e)
implies sup PreNorms h1 <= e by SEQ_4:62;
hence ||.vseq.n-tv.|| <=e by A55,A531,ThB17;
end;
end;
for e be Real st e > 0
ex m be Element of NAT st for n be Element of NAT st
n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A59: e > 0;
A60:e/2 > 0 by A59,SEQ_2:3;
A61:e/2= m holds ||.(vseq.n) - tv.|| <= e/2 by A50,A60;
take m;
hereby let n be Element of NAT such that
A63: n >= m;
||.(vseq.n) - tv.|| <= e/2 by A62,A63;
hence ||.(vseq.n) - tv.|| < e by A61,XXREAL_0:2;
end;
end;
hence thesis by NORMSP_1:def 9;
end;
theorem ThB29:
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 ThB28;
hence thesis by LOPBAN_1:def 16;
end;
registration let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> complete;
coherence by ThB29;
end;
theorem
R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
proof
set B = R_Normed_Algebra_of_BoundedFunctions X;
set X1 = BoundedFunctions X;
reconsider B as non empty Normed_Algebra by LmAlgebra4;
A1:now let f,g being Element of B;
f in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
A01: f1=f & f1 is_bounded_on X;
g in BoundedFunctions X; then
consider g1 be Function of X,REAL such that
A02: g1=g & g1 is_bounded_on X;
f*g in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A03: h1=f*g & h1 is_bounded_on X;
A04:PreNorms f1 is non empty bounded_above &
PreNorms g1 is non empty bounded_above &
PreNorms h1 is non empty bounded_above by A01,A02,A03,ThB13;
B01:||.f.|| = sup PreNorms f1 by A01,ThB17;
B02:||.g.|| = sup PreNorms g1 by A02,ThB17;
now let s be real number;
assume s in PreNorms h1; then
consider t be Element of X such that
E1: s = abs(h1.t);
abs(h1.t) = abs(f1.t * g1.t) by A01,A02,A03,ThB23a; then
E2: abs(h1.t) = abs(f1.t)*abs(g1.t) by COMPLEX1:151;
E3: 0 <= abs(f1.t) & 0 <= abs(g1.t) by COMPLEX1:132;
abs(f1.t) in PreNorms f1; then
E4: abs(f1.t) <= sup PreNorms f1 by A04,SEQ_4:def 4; then
E5: abs(f1.t)*abs(g1.t) <= (sup PreNorms f1)*abs(g1.t) by E3,XREAL_1:66;
E6: 0 <= sup PreNorms f1 by E4,COMPLEX1:132;
abs(g1.t) in PreNorms g1; then
abs(g1.t) <= sup PreNorms g1 by A04,SEQ_4:def 4; then
(sup PreNorms f1)*abs(g1.t) <= (sup PreNorms f1)*(sup PreNorms g1)
by E6,XREAL_1:66;
hence s <= (sup PreNorms f1)*(sup PreNorms g1) by E1,E2,E5,XXREAL_0:2;
end; then
sup PreNorms h1 <= (sup PreNorms f1)*(sup PreNorms g1) by SEQ_4:62;
hence ||. f*g .|| <= ||.f.|| * ||.g.|| by B01,B02,A03,ThB17;
end;
1.B in BoundedFunctions X; then
consider ONE be Function of X,REAL such that
A21:ONE = 1.B & ONE is_bounded_on X;
1.B = 1_R_Algebra_of_BoundedFunctions X; then
A22:1.B = X --> 1 by ThB12One;
for s be set holds s in PreNorms ONE iff s = 1
proof
let s be set;
hereby assume s in PreNorms ONE; then
consider t be Element of X such that
A23: s = abs((X-->1).t) by A21,A22;
(X-->1).t = 1 by FUNCOP_1:13;
hence s = 1 by A23,COMPLEX1:134;
end;
assume A24:s = 1;
consider t be Element of X;
(X-->1).t = 1 by FUNCOP_1:13; then
s = abs((X-->1).t) by A24,COMPLEX1:134;
hence s in PreNorms ONE by A21,A22;
end; then
PreNorms ONE = {1} by TARSKI:def 1; then
sup PreNorms ONE = 1 by SEQ_4:22; then
A2:||. 1.B .|| = 1 by A21,ThB17;
A3:now let a be Real, f,g be Element of B;
f in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
A31: f1=f & f1 is_bounded_on X;
g in BoundedFunctions X; then
consider g1 be Function of X,REAL such that
A32: g1=g & g1 is_bounded_on X;
a*g in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A33: h1=a*g & h1 is_bounded_on X;
f*g in BoundedFunctions X; then
consider h2 be Function of X,REAL such that
A34: h2=f*g & h2 is_bounded_on X;
a*(f*g) in BoundedFunctions X; then
consider h3 be Function of X,REAL such that
A35: h3=a*(f*g) & h3 is_bounded_on X;
now let x be Element of X;
h3.x = a*h2.x by A34,A35,ThB23; then
h3.x = a * (f1.x * g1.x) by A31,A32,A34,ThB23a; then
h3.x = f1.x * (a * g1.x);
hence h3.x = f1.x * h1.x by A32,A33,ThB23;
end;
hence a*(f*g) = f*(a*g) by A31,A33,A35,ThB23a;
end;
A4:now let f,g,h be Element of B;
f in BoundedFunctions X; then
consider f1 be Function of X,REAL such that
A41: f1=f & f1 is_bounded_on X;
g in BoundedFunctions X; then
consider g1 be Function of X,REAL such that
A42: g1=g & g1 is_bounded_on X;
h in BoundedFunctions X; then
consider h1 be Function of X,REAL such that
A43: h1=h & h1 is_bounded_on X;
g+h in BoundedFunctions X; then
consider gPh1 be Function of X,REAL such that
A44: gPh1=g+h & gPh1 is_bounded_on X;
g*f in BoundedFunctions X; then
consider gf1 be Function of X,REAL such that
A45: gf1=g*f & gf1 is_bounded_on X;
h*f in BoundedFunctions X; then
consider hf1 be Function of X,REAL such that
A46: hf1=h*f & hf1 is_bounded_on X;
(g+h)*f in BoundedFunctions X; then
consider F1 be Function of X,REAL such that
A47: F1=(g+h)*f & F1 is_bounded_on X;
now let x be Element of X;
F1.x = gPh1.x * f1.x by A44,A41,A47,ThB23a; then
F1.x = (g1.x + h1.x) * f1.x by A42,A43,A44,ThB22; then
F1.x = g1.x * f1.x + h1.x * f1.x; then
F1.x = gf1.x + h1.x * f1.x by A41,A42,A45,ThB23a;
hence F1.x = gf1.x + hf1.x by A41,A43,A46,ThB23a;
end;
hence (g+h)*f = g*f + h*f by A45,A46,A47,ThB22;
end;
A5:for f be Element of B holds 1.B * f = f by UNITAL;
B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital complete Normed_Algebra
by A1,A2,A3,A4,A5,LOPBAN_2:def 9,def 10,def 11,VECTSP_1:def 12,def 19;
hence thesis;
end;