:: Banach Algebra of Bounded Complex-Valued Functionals
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 20, 2010
:: Copyright (c) 2010-2011 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 STRUCT_0, XREAL_0, ORDINAL1, FUNCOP_1, NUMBERS, PRE_TOPC,
ORDINAL2, SUBSET_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
ARYTM_1, COMPLEX1, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1,
IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, BINOP_1, SUPINF_2, GROUP_1,
REALSET1, ZFMISC_1, XXREAL_2, XXREAL_0, NORMSP_1, REWRITE1, NAT_1,
RSSPACE3, SEQ_2, PARTFUN1, SEQ_1, LOPBAN_1, SEQ_4, CFUNCDOM, CLVECT_1,
VECTSP_1, RELAT_2, CC0SP1, CFUNCT_1, CLOPBAN2, LOPBAN_2, METRIC_1,
COMSEQ_1, CSSPACE4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, NUMBERS,
XXREAL_0, XREAL_0, REAL_1, COMPLEX1, BINOP_2, XXREAL_2, REALSET1,
VALUED_1, SEQ_1, SEQ_2, SEQ_4, CFUNCT_1, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, IDEAL_1, CLVECT_1, CFUNCDOM,
CLOPBAN2, C0SP1, CLOPBAN1, COMSEQ_1, CSSPACE3, COMSEQ_2;
constructors REAL_1, REALSET1, COMPLEX1, IDEAL_1, SEQ_1, C0SP1, PARTFUN3,
BINOP_2, TOPMETR, SEQ_4, MEASURE6, CLOPBAN2, CSSPACE3, COMSEQ_2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0,
NUMBERS, ORDINAL1, MEMBERED, RELAT_1, VECTSP_1, VECTSP_2, VALUED_0,
C0SP1, XXREAL_0, FUNCT_2, VALUED_1, RFUNCT_1, COMPLEX1, FUNCOP_1,
CFUNCDOM, CLVECT_1, XCMPLX_0, COMSEQ_2, CLOPBAN2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions REALSET1, ALGSTR_0, TARSKI, XCMPLX_0, RLVECT_1, VECTSP_1,
STRUCT_0, GROUP_1, BINOP_1, VALUED_1, C0SP1, CFUNCDOM, CLVECT_1,
COMPLEX1, NORMSP_0;
theorems RFUNCT_1, FUNCT_1, SEQ_2, ALGSTR_0, COMPLEX1, ZFMISC_1, TARSKI,
IDEAL_1, RELAT_1, XREAL_0, XXREAL_0, FUNCT_2, XBOOLE_0, XREAL_1,
XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, GROUP_1, VALUED_1, C0SP1, SEQ_4,
XXREAL_2, CFUNCDOM, CLVECT_1, RELSET_1, RSSPACE2, CFUNCT_1, CLOPBAN2,
NORMSP_0, CSSPACE3, COMSEQ_3, COMSEQ_2, CFCONT_1, CLOPBAN1;
schemes SEQ_1, FUNCT_2;
begin :: Banach Algebra of Bounded Complex-Valued Functionals
definition
let V be ComplexAlgebra;
mode ComplexSubAlgebra of V -> ComplexAlgebra means :DefComplexAlgebra:
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) | [:COMPLEX,the carrier of it:]
& 1.it = 1.V & 0.it = 0.V;
existence
proof
take V;
thus thesis by RELSET_1:34;
end;
end;
theorem Th1:
for X being non empty set,
V being ComplexAlgebra,
V1 being non empty Subset of V,
d1,d2 being Element of X,
A being BinOp of X,
M being Function of [:X,X:],X,
MR being Function of [:COMPLEX,X:],X st
(V1 = X & d1 = 0.V & d2 = 1.V
& A = (the addF of V)||V1 & M = (the multF of V)||V1
& MR = (the Mult of V) | [:COMPLEX,V1:]
& V1 is having-inverse)
holds ComplexAlgebraStr(#X,M,A,MR,d2,d1#) is ComplexSubAlgebra of V
proof
let X be non empty set, V be ComplexAlgebra,
V1 be non empty Subset of V, d1,d2 be Element of X,
A be BinOp of X, M be Function of [:X,X:],X,
MR be Function of [:COMPLEX,X:],X;
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) | [:COMPLEX,V1:] and
A7: for v be Element of V st v in V1 holds -v in V1;
reconsider W = ComplexAlgebraStr(# X,M,A,MR,d2,d1#)
as non empty ComplexAlgebraStr;
A9: now
let x,y be Element of W;
reconsider x1 = x, y1 = y as Element of V by A1,TARSKI:def 3;
x + y = (the addF of V).([x,y]) by A1,A4,FUNCT_1:72;
hence x + y = (the addF of V).(x,y);
end;
A10: now
let a,x be VECTOR of W;
a * x = (the multF of V).([a,x]) by A1,A5,FUNCT_1:72;
hence a * x = (the multF of V).(a,x);
end;
A12: 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 MV = the Mult 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 A9;
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 A9; then
A13: x + (y + z) = x1 + (y1 + z1) by A9;
(x + y) + z = Av.(x + y,z1) by A9;
then (x + y) + z = (x1 + y1) + z1 by A9;
hence (x + y) + z = x + (y + z) by A13,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,A9
.= 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
A14: x1 + v = 0.V by ALGSTR_0:def 11;
v = - x1 by A14,VECTSP_1:63;
then reconsider y = v as Element of W by A1,A7;
take y;
thus thesis by A2,A9,A14;
end;
hereby
let v,w be 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 A10;
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 A10; then
A15: a * (b * x) = a1 * (b1 * y) by A10;
a * b = a1 * b1 by A10;
then (a * b) * x = (a1 * b1) * y by A10;
hence (a * b) * x = a * (b * x) by A15,GROUP_1:def 4;
end;
hereby
let v be Element of W;
reconsider v1 = v as Element of V by A1,TARSKI:def 3;
v * 1.W =v1*1.V by A3,A10;
hence v * 1.W = v by VECTSP_1:def 13;
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;
y+z = y1+z1 by A9;
then x*(y+z) = x1*(y1+z1) by A10; then
A16: x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 11;
x*y = x1*y1 & x*z = x1*z1 by A10;
hence x*(y+z) = x*y + x*z by A9,A16;
end;
C: for a be Complex,x,y be VECTOR of W holds a*(x+y) = a*x + a*y
proof
let a be Complex;
let x,y be VECTOR of W;
reconsider x1=x, y1=y as Element of V by A1,TARSKI:def 3;
A17: a*x = (the Mult of V).(a,x) by A1,A6,FUNCT_1:72
.=a*x1;
A18: a*y = (the Mult of V).(a,y) by A1,A6,FUNCT_1:72
.= a*y1;
a*(x+y) = (the Mult of V).(a,x+y) by A1,A6,FUNCT_1:72
.= a*(x1+y1) by A9; then
a*(x+y) =a*x1 + a*y1 by CLVECT_1:def 2;
hence thesis by A9,A17,A18;
end;
B: for a,b be Complex,v be VECTOR of W holds (a + b) * v = a * v + b * v
proof
let a,b be Complex;
let x be Element of W;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
A21: a*x = (the Mult of V).(a,x) by A1,A6,FUNCT_1:72
.= a*x1;
A22: b*x = (the Mult of V).(b,x) by A1,A6,FUNCT_1:72
.= b*x1;
(a+b)*x = (the Mult of V).(a+b,x) by A1,A6,FUNCT_1:72
.= (a+b)*x1;
then (a+b)*x = a*x1 + b*x1 by CLVECT_1:def 3;
hence (a+b)*x =a*x + b*x by A9,A21,A22;
end;
A: for a,b be Complex,v be VECTOR of W holds (a * b) * v = a * (b * v)
proof
let a,b be Complex;
let x be Element of W;
reconsider x1=x as Element of V by A1,TARSKI:def 3;
reconsider y=b*x as Element of W;
reconsider y1=b*x1 as Element of V;
A24: b*x = (the Mult of V).(b,x) by A1,A6,FUNCT_1:72
.= b*x1;
A25: a*(b*x) = (the Mult of V).(a,y) by A1,A6,FUNCT_1:72
.= a*(b*x1) by A24;
(a*b)*x = (the Mult of V).(a*b,x) by A1,A6,FUNCT_1:72
.= (a*b)*x1;
hence thesis by A25,CLVECT_1:def 4;
end;
for x,y be Element of W,a be Complex holds a * (x * y) = (a * x) * y
proof
let x,y be Element of W;
let a being Complex;
reconsider x1=x, y1=y as Element of V by A1,TARSKI:def 3;
set z=x*y;
set z1=x1*y1;
A28: a*x =(the Mult of V).(a,x) by A1,A6,FUNCT_1:72
.= a*x1;
A30: a*(x*y) = (the Mult of V).(a,z) by A1,A6,FUNCT_1:72
.= a*(x1*y1) by A10;
a * (x1 * y1) = (a * x1) * y1 by CFUNCDOM:def 9;
hence thesis by A10,A28,A30;
end;
hence thesis by C,B,A,CFUNCDOM:def 9,CLVECT_1:def 2,def 3,def 4;
end;
0.W = 0.V & 1.W= 1.V by A2,A3;
hence thesis by A1,A4,A5,A6,A12,DefComplexAlgebra;
end;
registration let V be ComplexAlgebra;
cluster strict ComplexSubAlgebra of V;
existence
proof
set V1 = [#]V;
A1: the Mult of V = (the Mult of V) | [:COMPLEX,V1:] by RELSET_1:34;
the addF of V = (the addF of V)||V1 &
the multF of V = (the multF of V)||V1 by RELSET_1:34; then
ComplexAlgebraStr(#the carrier of V, the multF of V, the addF of V,
the Mult of V, 1.V, 0.V #) is ComplexSubAlgebra of V by A1,Th1;
hence thesis;
end;
end;
definition let V be ComplexAlgebra, V1 be Subset of V;
attr V1 is Cadditively-linearly-closed means :Def10:
V1 is add-closed having-inverse &
for a be Complex, v be Element of V st v in V1 holds a * v in V1;
end;
definition let V be ComplexAlgebra, V1 be Subset of V such that
A1: V1 is Cadditively-linearly-closed non empty;
func Mult_(V1,V) -> Function of [:COMPLEX,V1:], V1 equals :Def11:
(the Mult of V) | [:COMPLEX,V1:];
correctness
proof
A2: [:COMPLEX,V1:] c= [:COMPLEX,the carrier of V:]
& dom(the Mult of V) = [:COMPLEX,the carrier of V:]
by FUNCT_2:def 1,ZFMISC_1:118;
A3: for z be set st z in [:COMPLEX,V1:]
holds ((the Mult of V) | [:COMPLEX,V1:]).z in V1
proof
let z be set such that
A4: z in [:COMPLEX,V1:];
consider r,x be set such that
A5: r in COMPLEX and
A6: x in V1 and
A7: z=[r,x] by A4,ZFMISC_1:def 2;
reconsider r as Complex by A5;
reconsider y=x as VECTOR of V by A6;
[r,x] in dom((the Mult of V) | [:COMPLEX,V1:]) by A2,A4,A7,RELAT_1:91;
then ((the Mult of V) | [:COMPLEX,V1:]).z = r*y by A7,FUNCT_1:70;
hence thesis by A1,A6,Def10;
end;
dom((the Mult of V) | [:COMPLEX,V1:])=[:COMPLEX,V1:] by A2,RELAT_1:91;
hence thesis by A3,FUNCT_2:5;
end;
end;
definition let X be non empty set;
func ComplexBoundedFunctions(X) -> non empty Subset of CAlgebra X equals
{ f where f is Function of X,COMPLEX : f|X is bounded };
correctness
proof
A1:{ f where f is Function of X,COMPLEX : f|X is bounded } c= Funcs(X,COMPLEX)
proof
let x be set;
assume x in { f where f is Function of X,COMPLEX : f|X is bounded }; then
ex f be Function of X,COMPLEX st x=f & f|X is bounded;
hence x in Funcs(X,COMPLEX) by FUNCT_2:11;
end;
{ f where f is Function of X,COMPLEX : f|X is bounded } is non empty
proof
reconsider g = X --> 0c as Function of X,COMPLEX;
g|X is bounded; then
g in { f where f is Function of X,COMPLEX : f|X is bounded };
hence thesis;
end;
hence thesis by A1;
end;
end;
registration let X be non empty set;
cluster CAlgebra X -> scalar-unital;
coherence
proof
for v being Element of CAlgebra(X) holds 1r * v = v by CFUNCDOM:14;
hence thesis by CLVECT_1:def 5;
end;
end;
registration let X be non empty set;
cluster ComplexBoundedFunctions(X) -> Cadditively-linearly-closed
multiplicatively-closed;
coherence
proof
set W = ComplexBoundedFunctions X;
set V = CAlgebra X;
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 & u in W;
consider v1 be Function of X,COMPLEX such that
A3: v1=v & v1|X is bounded by A2;
consider u1 be Function of X,COMPLEX such that
A4: u1=u & u1|X is bounded by A2;
dom(v1+u1) = X /\ X by FUNCT_2:def 1; then
A5: v1+u1 is Function of X,COMPLEX & (v1+u1)|X is bounded
by A3,A4,CFUNCT_1:87;
reconsider h = v+u as Element of Funcs(X,COMPLEX);
A6: ex f being Function st h = f & dom f = X & rng f c= COMPLEX
by FUNCT_2:def 2;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1; then
A7: 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 A3,A4,CFUNCDOM:1; then
v+u=v1+u1 by A7,A6,VALUED_1:def 1;
hence v+u in W by A5;
end; then
A8: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
A9: v in W;
consider v1 be Function of X,COMPLEX such that
A10: v1=v & v1|X is bounded by A9;
A11: -v1 is Function of X,COMPLEX & (-v1)|X is bounded
by A10,CFUNCT_1:86;
reconsider h = -v, v2 = v as Element of Funcs(X,COMPLEX);
A12: h=(-1r)*v by CLVECT_1:4;
A13: ex f being Function st h = f & dom f = X & rng f c= COMPLEX
by FUNCT_2:def 2;
A14: 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 = (-1r)*(v2.y) by A12,CFUNCDOM:6;
hence h.x = -v1.x by A10;
end; then
-v=-v1 by A14,A13,VALUED_1:9;
hence -v in W by A11;
end; then
A15:W is having-inverse by C0SP1:def 1;
for a be Complex, u be Element of V st u in W holds a * u in W
proof
let a be Complex, u be Element of V such that
A16: u in W;
consider u1 be Function of X,COMPLEX such that
A17:u1=u & u1|X is bounded by A16;
A18:a(#)u1 is Function of X,COMPLEX & (a(#)u1)|X is bounded
by A17,CFUNCT_1:84;
reconsider h = a*u as Element of Funcs(X,COMPLEX);
A19:ex f being Function st h = f & dom f = X & rng f c= COMPLEX
by FUNCT_2:def 2;
A20:dom u1 = X by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = a*(u1.x) by A17,CFUNCDOM:6; then
a*u=a(#)u1 by A20,A19,VALUED_1:def 5;
hence a*u in W by A18;
end;
hence ComplexBoundedFunctions(X) is Cadditively-linearly-closed
by A8,A15,Def10;
A21: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
A22: v in W & u in W;
consider v1 be Function of X,COMPLEX such that
A23:v1=v & v1|X is bounded by A22;
consider u1 be Function of X,COMPLEX such that
A24:u1=u & u1|X is bounded by A22;
dom(v1(#)u1) = X /\ X by FUNCT_2:def 1; then
A25:v1(#)u1 is Function of X,COMPLEX & (v1(#)u1)|X is bounded
by A23,A24,CFUNCT_1:88;
reconsider h = v*u as Element of Funcs(X,COMPLEX);
A26:ex f being Function st h = f & dom f = X & rng f c= COMPLEX
by FUNCT_2:def 2;
dom v1 /\ dom u1 = X /\ dom u1 by FUNCT_2:def 1; then
A27: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 A23,A24,CFUNCDOM:2; then
v*u=v1(#)u1 by A27,A26,VALUED_1:def 4;
hence v*u in W by A25;
end;
reconsider g = ComplexFuncUnit X as Function of X,COMPLEX;
g|X is bounded; then
1.V in W;
hence thesis by A21,C0SP1:def 4;
end;
end;
registration let V be ComplexAlgebra;
cluster Cadditively-linearly-closed multiplicatively-closed
(non empty Subset of V);
existence
proof
reconsider W = [#]V as non empty Subset of V;
W is add-closed having-inverse &
for a be Complex, v be Element of V st v in W holds a * v in W; then
A1: W is Cadditively-linearly-closed by Def10;
1.V in W & for v,u be Element of V st v in W & u in W holds v * u in W;
then W is multiplicatively-closed by C0SP1:def 4;
hence thesis by A1;
end;
end;
definition let V be non empty CLSStruct;
attr V is scalar-mult-cancelable means
for a be Complex, v be Element of V st a*v=0.V holds a=0 or v=0.V;
end;
theorem Th2:
for V being ComplexAlgebra,
V1 being Cadditively-linearly-closed multiplicatively-closed
(non empty Subset of V) holds
ComplexAlgebraStr(# V1,mult_(V1,V), Add_(V1,V), Mult_(V1,V), One_(V1,V),
Zero_(V1,V) #) is ComplexSubAlgebra of V
proof
let V be ComplexAlgebra,
V1 be Cadditively-linearly-closed multiplicatively-closed
(non empty Subset of V);
A2: Mult_(V1,V) = (the Mult of V) | [:COMPLEX,V1:] by Def11;
A3: V1 is add-closed having-inverse non empty by Def10;
A4: One_(V1,V) =1_V & mult_(V1,V) = (the multF of V) || V1
by C0SP1:def 6,def 8;
Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1
by A3,C0SP1:def 5,def 7;
hence thesis by A2,A3,A4,Th1;
end;
theorem Th4:
for V be ComplexAlgebra, V1 be ComplexSubAlgebra 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 Complex st
v1=v holds a*v1=a*v ) &
1_V1 = 1_V & 0.V1=0.V
proof
let V be ComplexAlgebra, V1 be ComplexSubAlgebra of V;
hereby let x1,y1 be Element of V1, x,y be Element of V;
assume
AS1:x1=x & y1=y;
x1 + y1 = ((the addF of V)||the carrier of V1).([x1,y1])
by DefComplexAlgebra;
hence x1 + y1 = x+y by AS1,FUNCT_1:72;
end;
hereby let x1,y1 be Element of V1, x,y be Element of V;
assume
AS2:x1=x & y1=y;
x1 * y1 = ((the multF of V)||the carrier of V1).([x1,y1])
by DefComplexAlgebra;
hence x1 * y1 = x*y by AS2,FUNCT_1:72;
end;
hereby let v1 be Element of V1, v be Element of V, a be Complex;
assume
AS3:v1 = v;
a * v1 = ((the Mult of V) | [:COMPLEX,the carrier of V1:]).([a,v1])
by DefComplexAlgebra;
hence a * v1 = a * v by AS3,FUNCT_1:72;
end;
thus thesis by DefComplexAlgebra;
end;
definition let X be non empty set;
func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals
ComplexAlgebraStr (#
ComplexBoundedFunctions(X),
mult_(ComplexBoundedFunctions(X),CAlgebra(X)),
Add_(ComplexBoundedFunctions(X),CAlgebra(X)),
Mult_(ComplexBoundedFunctions(X),CAlgebra(X)),
One_(ComplexBoundedFunctions(X),CAlgebra(X)),
Zero_(ComplexBoundedFunctions(X),CAlgebra(X)) #);
coherence by Th2;
end;
theorem
for X being non empty set holds C_Algebra_of_BoundedFunctions(X) is
ComplexSubAlgebra of CAlgebra(X) by Th2;
registration let X be non empty set;
cluster C_Algebra_of_BoundedFunctions(X) ->
vector-distributive scalar-unital;
coherence
proof
now let v be VECTOR of C_Algebra_of_BoundedFunctions(X);
reconsider v1=v as VECTOR of CAlgebra X by TARSKI:def 3;
C_Algebra_of_BoundedFunctions(X) is ComplexSubAlgebra of CAlgebra(X)
by Th2;
then 1r * v = 1r*v1 by Th4;
hence 1r * v =v by CFUNCDOM:14;
end;
hence thesis by CLVECT_1:def 5;
end;
end;
theorem Th8:
for X being non empty set,
F, G, H being VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g, h being Function of X,COMPLEX st f=F & g=G & h=H holds
( H = F+G iff (for x be Element of X holds h.x = (f.x) + (g.x)) )
proof
let X be non empty set,
F, G, H be VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g, h be Function of X,COMPLEX;
assume
A1: f=F & g=G & h=H;
A2:C_Algebra_of_BoundedFunctions(X) is ComplexSubAlgebra of CAlgebra(X)
by Th2;
reconsider f1=F, g1=G, h1=H as VECTOR of CAlgebra(X) by TARSKI:def 3;
hereby assume
A3: H = F+G;
let x be Element of X;
h1=f1+g1 by A2,A3,Th4;
hence h.x = f.x+g.x by A1,CFUNCDOM:1;
end;
assume for x be Element of X holds h.x = f.x+g.x; then
h1=f1+g1 by A1,CFUNCDOM:1;
hence H =F+G by A2,Th4;
end;
theorem Th9:
for X being non empty set, a being Complex,
F, G being VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g being Function of X,COMPLEX st f=F & g=G holds
( G = a*F iff for x be Element of X holds g.x = a*(f.x) )
proof
let X be non empty set,
a be Complex,
F, G be VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g be Function of X,COMPLEX;
assume
A1: f=F & g=G;
A2:C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
reconsider f1=F, g1=G as VECTOR of CAlgebra X by TARSKI:def 3;
hereby assume
A3: G = a*F;
let x be Element of X;
g1=a*f1 by A2,A3,Th4;
hence g.x=a*f.x by A1,CFUNCDOM:6;
end;
assume for x be Element of X holds g.x=a*f.x; then
g1=a*f1 by A1,CFUNCDOM:6;
hence G =a*F by A2,Th4;
end;
theorem Th10:
for X being non empty set,
F, G, H being VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g, h being Function of X,COMPLEX st f=F & g=G & h=H holds
( H = F*G iff for x be Element of X holds h.x = (f.x)*(g.x))
proof
let X be non empty set,
F, G, H be VECTOR of C_Algebra_of_BoundedFunctions(X),
f, g, h be Function of X,COMPLEX;
assume
A1:f=F & g=G & h=H;
A2:C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
reconsider f1=F, g1=G, h1=H as VECTOR of CAlgebra X by TARSKI:def 3;
hereby assume
A3: H = F*G;
let x be Element of X;
h1 = f1*g1 by A2,A3,Th4;
hence h.x = f.x * g.x by A1,CFUNCDOM:2;
end;
assume for x be Element of X holds h.x = f.x * g.x; then
h1 = f1 * g1 by A1,CFUNCDOM:2;
hence H = F * G by A2,Th4;
end;
theorem Th11:
for X being non empty set holds
0.C_Algebra_of_BoundedFunctions X = X -->0
proof
let X be non empty set;
A1:C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
0.CAlgebra X = X -->0;
hence thesis by A1,Th4;
end;
theorem Th12:
for X being non empty set holds
1_C_Algebra_of_BoundedFunctions X = X --> 1r
proof
let X be non empty set;
A1:C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
1_CAlgebra X = X -->1r;
hence thesis by A1,Th4;
end;
definition let X be non empty set, F be set;
assume
A1: F in ComplexBoundedFunctions(X);
func modetrans(F,X) -> Function of X,COMPLEX means :DefB7:
it = F & it|X is bounded;
correctness by A1;
end;
definition let X be non empty set, f be Function of X,COMPLEX;
func PreNorms f -> non empty Subset of REAL equals
{ |.f.x.| where x is Element of X : not contradiction };
coherence
proof
A1:now let z be set;
now assume z in {|.f.x.| where x is Element of X : not contradiction };
then ex x be Element of X st z=|.f.x.|;
hence z in REAL;
end;
hence z in {|.f.x.| where x is Element of X : not contradiction }
implies z in REAL;
end;
set z = the Element of X;
|.f.z.| in {|.f.x.| where x is Element of X : not contradiction };
hence thesis by A1,TARSKI:def 3;
end;
end;
Lm1:
for C being non empty set,
f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
proof
let C be non empty set,
f be PartFunc of C,COMPLEX;
A1: dom f = dom |.f.| by VALUED_1:def 11;
thus |.f.| is bounded implies f is bounded
proof
assume |.f.| is bounded;
then consider r1 being real number such that
A3: for y being set st y in dom |.f.| holds
|.(|.f.| .y).| < r1 by SEQ_2:def 5;
now let y be set;
assume
A5: y in dom f;
then |.(|.f.|.y).| < r1 by A1,A3;
then |.|.(f.y).|.| < r1 by A1,A5,VALUED_1:def 11;
hence not r1 <= |.(f.y).|;
end;
hence thesis by SEQ_2:def 5;
end;
assume f is bounded;
then consider r2 being real number such that
A7: for y being set st y in dom f holds |.(f.y).| < r2 by SEQ_2:def 5;
now
take r2;
let y be set;
assume
A8: y in dom |.f.|;
then |.|.(f.y).|.| < r2 by A1,A7;
hence |.(|.f.|.y).| < r2 by A8,VALUED_1:def 11;
end;
hence |.f.| is bounded by SEQ_2:def 5;
end;
theorem Th13:
for X being non empty set,
f being Function of X,COMPLEX st f | X is bounded holds
PreNorms f is bounded_above
proof
let X be non empty set,
f be Function of X,COMPLEX;
A1: dom |.f.| = dom f by VALUED_1:def 11;
A2: dom (|.f.| | X) = X /\ (dom |.f.|) by RELAT_1:90;
A3: |.f.| | X = |.(f | X).| by RFUNCT_1:62;
assume f|X is bounded;
then |.f.| | X is bounded by A3,Lm1;
then consider p being real number such that
A4: for c being set st c in dom (|.f.| | X) holds
|.((|.f.| | X).c).| <= p by RFUNCT_1:89;
A5:now
let c be Element of X;
assume
A6:c in X /\ (dom f);
|.((|.f.| | X).c).| = |.(|.f.|.c).| by A1,A2,A6,FUNCT_1:70
.= |.|.(f.c).|.| by VALUED_1:18;
hence |.(f.c).| <= p by A1,A2,A4,A6;
end;
A7:X /\ dom f = X /\ X by FUNCT_2:def 1;
A8:now let r be ext-real number;
assume r in PreNorms f; then
consider t be Element of X such that
A9:r=|.f.t.|;
thus r <=p by A7,A9,A5;
end;
p is UpperBound of (PreNorms f) by A8,XXREAL_2:def 1;
hence thesis by XXREAL_2:def 10;
end;
theorem Th14:
for X being non empty set,
f being Function of X,COMPLEX holds
f|X is bounded iff PreNorms f is bounded_above
proof
let X be non empty set,
f be Function of X,COMPLEX;
now assume
A1:PreNorms f is bounded_above;
reconsider K = upper_bound PreNorms f as Real;
A2:now let t be Element of X;
assume t in X /\ dom f;
|.f.t.| in PreNorms f;
hence |.(f/.t).| <= K by A1,SEQ_4:def 4;
end;
take K;
thus f|X is bounded by A2,CFUNCT_1:81;
end;
hence thesis by Th13;
end;
theorem Th15:
for X being non empty set
ex NORM be Function of ComplexBoundedFunctions(X),REAL st
for F be set st F in ComplexBoundedFunctions(X) holds
NORM.F = upper_bound PreNorms(modetrans(F,X))
proof
let X be non empty set;
deffunc F(set) = upper_bound PreNorms(modetrans($1,X));
A1:for z be set st z in ComplexBoundedFunctions(X) holds F(z) in REAL;
ex f being Function of ComplexBoundedFunctions(X),REAL st
for x being set st x in ComplexBoundedFunctions(X) holds
f.x = F(x) from FUNCT_2:sch 2(A1);
hence thesis;
end;
definition let X be non empty set;
func ComplexBoundedFunctionsNorm(X) ->
Function of ComplexBoundedFunctions(X),REAL means:DefB9C:
for x be set st x in ComplexBoundedFunctions(X) holds
it.x = upper_bound PreNorms(modetrans(x,X));
existence by Th15;
uniqueness
proof
let NORM1,NORM2 be Function of ComplexBoundedFunctions(X),REAL such that
A1:for x be set st x in ComplexBoundedFunctions(X) holds
NORM1.x = upper_bound PreNorms(modetrans(x,X)) and
A2:for x be set st x in ComplexBoundedFunctions(X) holds
NORM2.x = upper_bound PreNorms(modetrans(x,X));
A3:dom NORM1 = ComplexBoundedFunctions(X) &
dom NORM2 = ComplexBoundedFunctions(X) by FUNCT_2:def 1;
for z be set st z in ComplexBoundedFunctions(X) holds NORM1.z = NORM2.z
proof
let z be set such that
A4: z in ComplexBoundedFunctions(X);
NORM1.z = upper_bound PreNorms(modetrans(z,X)) by A1,A4;
hence thesis by A2,A4;
end;
hence thesis by A3,FUNCT_1:9;
end;
end;
theorem Th16:
for X being non empty set,
f being Function of X,COMPLEX st f|X is bounded holds
modetrans(f,X) = f
proof
let X be non empty set,
f be Function of X,COMPLEX;
assume f|X is bounded; then
f in ComplexBoundedFunctions X;
hence thesis by DefB7;
end;
theorem Th17:
for X being non empty set,
f being Function of X,COMPLEX st f|X is bounded holds
(ComplexBoundedFunctionsNorm(X)).f = upper_bound PreNorms f
proof
let X be non empty set,
f be Function of X,COMPLEX;
assume
A1:f|X is bounded; then
f in ComplexBoundedFunctions(X); then
(ComplexBoundedFunctionsNorm(X)).f = upper_bound PreNorms(modetrans(f,X))
by DefB9C;
hence thesis by Th16,A1;
end;
definition let X be non empty set;
func C_Normed_Algebra_of_BoundedFunctions(X) -> Normed_Complex_AlgebraStr
equals
Normed_Complex_AlgebraStr(# ComplexBoundedFunctions(X),
mult_(ComplexBoundedFunctions(X),CAlgebra(X)),
Add_(ComplexBoundedFunctions(X),CAlgebra(X)),
Mult_(ComplexBoundedFunctions(X),CAlgebra(X)),
One_(ComplexBoundedFunctions(X),CAlgebra(X)),
Zero_(ComplexBoundedFunctions(X),CAlgebra(X)),
ComplexBoundedFunctionsNorm(X) #);
correctness;
end;
registration let X be non empty set;
cluster C_Normed_Algebra_of_BoundedFunctions(X) -> non empty;
correctness;
end;
Lm2:
now
let X be non empty set;
set F = C_Normed_Algebra_of_BoundedFunctions(X);
let x, e be Element of C_Normed_Algebra_of_BoundedFunctions(X);
set X1 = ComplexBoundedFunctions(X);
reconsider f = x as Element of ComplexBoundedFunctions(X);
assume
A1:e = One_(ComplexBoundedFunctions(X),CAlgebra(X));
then x*e=(mult_(ComplexBoundedFunctions(X),CAlgebra(X))).(f,1_CAlgebra(X))
by C0SP1:def 8;
then
A2:x*e=(the multF of (CAlgebra X))||(ComplexBoundedFunctions(X)).
(f,1_CAlgebra(X)) by C0SP1:def 6;
e*x=mult_(ComplexBoundedFunctions(X),CAlgebra(X)).(1_CAlgebra(X),f)
by A1,C0SP1:def 8; then
A3:e*x=(the multF of (CAlgebra X))||(ComplexBoundedFunctions(X)).
(1_CAlgebra(X),f) by C0SP1:def 6;
A4:1_CAlgebra(X) = 1_C_Algebra_of_BoundedFunctions(X) by Th12;
then [f,1_CAlgebra(X)]
in [:(ComplexBoundedFunctions(X)),(ComplexBoundedFunctions(X)):]
by ZFMISC_1:106;
then x*e = f * 1_CAlgebra(X) by A2,FUNCT_1:72;
hence x * e = x by VECTSP_1:def 13;
[1_CAlgebra(X),f]
in [:(ComplexBoundedFunctions(X)),(ComplexBoundedFunctions(X)):]
by A4,ZFMISC_1:106;
then e * x = 1_CAlgebra(X) * f by A3,FUNCT_1:72;
hence e * x = x by VECTSP_1:def 13;
end;
registration let X be non empty set;
cluster C_Normed_Algebra_of_BoundedFunctions(X) -> unital;
correctness
proof
reconsider e = One_(ComplexBoundedFunctions(X),CAlgebra(X)) as
Element of C_Normed_Algebra_of_BoundedFunctions(X);
take e;
thus thesis by Lm2;
end;
end;
theorem Th18:
for W being Normed_Complex_AlgebraStr,
V being ComplexAlgebra st
ComplexAlgebraStr(# the carrier of W,the multF of W,
the addF of W,the Mult of W,
the OneF of W,the ZeroF of W #) = V holds
W is ComplexAlgebra
proof
let W be Normed_Complex_AlgebraStr,
V be ComplexAlgebra;
assume
A1: ComplexAlgebraStr(# the carrier of W,the multF of W,
the addF of W,the Mult of W,
the OneF of W,the ZeroF of W #) = V;
reconsider W as non empty ComplexAlgebraStr by A1;
A2: W is right_unital
proof
let x be 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;
A3: W is right-distributive
proof
let x, y, z be 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;
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 being 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 x is right_complementable by ALGSTR_0:def 11;
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 4;
hence (a * b) * x = a * (b * x) by A1;
end;
A7: for v, w being Element of W holds v * w = w * v
proof
let v, w be 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;
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 6;
hence (x + y) + z = x + (y + z) 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 x + y = y + x by A1;
end;
A10: W is vector-distributive
proof
let a be Complex;
let x, y be VECTOR 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 CLVECT_1:def 2;
hence a * (x + y) = (a * x) + (a * y) by A1;
end;
A11: W is scalar-distributive
proof
let a, b be Complex;
let x be VECTOR 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 CLVECT_1:def 3;
hence (a + b) * x = (a * x) + (b * x) by A1;
end;
A12: W is scalar-associative
proof
let a, b be Complex;
let x be VECTOR 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 CLVECT_1:def 4;
hence (a * b) * x = a * (b * x) by A1;
end;
A13: W is vector-associative
proof
let x, y be VECTOR of W;
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Complex;
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by CFUNCDOM: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, 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;
hence thesis by A9,A8,A4,A7,A6,A2,A3,A10,A11,A12,A13,ALGSTR_0:def 16
,GROUP_1:def 4,def 16,RLVECT_1:def 5,def 6,def 7;
end;
theorem Th19:
for X being non empty set holds
C_Normed_Algebra_of_BoundedFunctions(X) is ComplexAlgebra
proof
let X be non empty set;
set W=C_Normed_Algebra_of_BoundedFunctions X;
set V=C_Algebra_of_BoundedFunctions X;
C_Algebra_of_BoundedFunctions X is ComplexAlgebra;
hence thesis by Th18;
end;
theorem
for X being non empty set,
F being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds
Mult_(ComplexBoundedFunctions(X),CAlgebra(X)).(1r,F) = F
proof
let X be non empty set,
F be Point of C_Normed_Algebra_of_BoundedFunctions(X);
set X1 = ComplexBoundedFunctions(X);
reconsider f1 = F as Element of ComplexBoundedFunctions(X);
A1: [1r,f1] in [:COMPLEX,(ComplexBoundedFunctions X):];
Mult_ (ComplexBoundedFunctions(X),CAlgebra(X)).(1r,F)
=((the Mult of CAlgebra(X)) | [:COMPLEX,ComplexBoundedFunctions(X):]).
(1r,f1) by Def11
.= (the Mult of CAlgebra(X)).(1r,f1) by A1,FUNCT_1:72
.= F by CFUNCDOM:14;
hence thesis;
end;
theorem Th21:
for X being non empty set holds
C_Normed_Algebra_of_BoundedFunctions(X) is ComplexLinearSpace
proof
let X be non empty set;
for v being Point of C_Normed_Algebra_of_BoundedFunctions(X)
holds 1r*v = v
proof
let v be Point of C_Normed_Algebra_of_BoundedFunctions(X);
reconsider v1 = v as Element of ComplexBoundedFunctions(X);
A2: 1r*v = ((the Mult of CAlgebra(X))|
[:COMPLEX,ComplexBoundedFunctions(X):]).([1r,v1]) by Def11
.= (the Mult of CAlgebra(X)).(1r,v1) by FUNCT_1:72
.= v1 by CFUNCDOM:14;
thus thesis by A2;
end;
hence thesis by Th19,CLVECT_1:def 5;
end;
theorem Th22:
for X being non empty set holds
X --> 0 = 0.(C_Normed_Algebra_of_BoundedFunctions(X))
proof
let X be non empty set;
X --> 0 = 0.(C_Algebra_of_BoundedFunctions(X)) by Th11;
hence thesis;
end;
theorem Th23:
for X being non empty set,
x being Element of X,
f being Function of X,COMPLEX,
F being Point of C_Normed_Algebra_of_BoundedFunctions(X) st
f = F & f | X is bounded holds |.f.x.| <= ||.F.||
proof
let X be non empty set,
x be Element of X,
f be Function of X,COMPLEX,
F be Point of C_Normed_Algebra_of_BoundedFunctions(X);
assume that
A1: f = F and
A2: f | X is bounded;
reconsider r=|.f.x.| as ext-real number;
A3:r in PreNorms f;
PreNorms f is non empty bounded_above by Th14,A2; then
r <= upper_bound PreNorms(f) by A3,SEQ_4:def 4;
hence |.f.x.| <= ||.F.|| by A1,A2,Th17;
end;
theorem
for X being non empty set,
F being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds
0 <= ||.F.||
proof
let X be non empty set,
F be Point of C_Normed_Algebra_of_BoundedFunctions(X);
F in ComplexBoundedFunctions X;
then consider g being Function of X,COMPLEX such that
A1: F = g and
A2: g | X is bounded;
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r1 = r0 as Real by A3;
now
let r be Real;
assume r in PreNorms g;
then ex t being Element of X st r = |.(g .t).|;
hence 0 <= r;
end;
then
A4: 0 <= r1 by A3;
PreNorms g is non empty bounded_above by Th14,A2;
then 0 <= upper_bound (PreNorms g) by A3,A4,SEQ_4:def 4;
hence 0 <= ||.F.|| by A1,A2,Th17;
end;
theorem Th25:
for X being non empty set,
F being Point of C_Normed_Algebra_of_BoundedFunctions(X) st
F = 0.(C_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
proof
let X be non empty set,
F be Point of C_Normed_Algebra_of_BoundedFunctions(X);
set z = X --> 0;
reconsider z = X --> 0c as Function of X,COMPLEX;
F in ComplexBoundedFunctions X;
then consider g being Function of X,COMPLEX such that
A1:g = F and
A2:g | X is bounded;
A3:( not PreNorms g is empty & PreNorms g is bounded_above ) by A2,Th14;
consider r0 being set such that
A4:r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A4;
A5:(for s be real number st s in PreNorms g holds s <= 0) implies upper_bound
PreNorms g <= 0 by SEQ_4:62;
assume
A6: F = 0.C_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,Th22; then
|.(g.t).| = |.(0).| by FUNCOP_1:13
.= 0;
hence 0 <= r & r <=0 by A8;
end; then
0<=r0 by A4; then
upper_bound (PreNorms g) = 0 by A7,A3,A4,A5,SEQ_4:def 4;
hence 0 = ||.F.|| by A1,A2,Th17;
end;
theorem Th26:
for X being non empty set,
f, g, h being Function of X,COMPLEX,
F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(X)
st f = F & g = G & h = H holds
(H = F+G iff for x being Element of X holds h.x = (f.x) + (g.x))
proof
let X be non empty set,
f, g, h be Function of X,COMPLEX,
F, G, H be Point of C_Normed_Algebra_of_BoundedFunctions(X);
reconsider f1 = F, g1 = G, h1 = H
as VECTOR of C_Algebra_of_BoundedFunctions(X);
A1: H = F + G iff h1 = f1 + g1;
assume f = F & g = G & h = H;
hence thesis by A1,Th8;
end;
theorem Th27:
for X being non empty set,
a being Complex,
f, g being Function of X,COMPLEX,
F, G being Point of C_Normed_Algebra_of_BoundedFunctions(X)
st f = F & g = G holds
( G = a*F iff for x being Element of X holds g.x = a*(f.x))
proof
let X be non empty set,
a be Complex,
f, g be Function of X,COMPLEX,
F, G be Point of C_Normed_Algebra_of_BoundedFunctions(X);
reconsider f1 = F, g1 = G as VECTOR of C_Algebra_of_BoundedFunctions(X);
A1: G = a * F iff g1 = a * f1;
assume f = F & g = G;
hence thesis by A1,Th9;
end;
theorem Th28:
for X being non empty set,
f, g, h being Function of X,COMPLEX,
F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(X)
st f = F & g = G & h = H holds
(H = F*G iff for x being Element of X holds h.x = (f.x)*(g.x))
proof
let X be non empty set,
f, g, h be Function of X,COMPLEX,
F, G, H be Point of C_Normed_Algebra_of_BoundedFunctions(X);
reconsider f1 = F, g1 = G, h1 = H
as VECTOR of C_Algebra_of_BoundedFunctions(X);
A1: H = F * G iff h1 = f1 * g1;
assume f = F & g = G & h = H;
hence thesis by A1,Th10;
end;
theorem Th29:
for X being non empty set,
a being Complex,
F, G being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds
((||.F.|| = 0 implies F = 0.C_Normed_Algebra_of_BoundedFunctions(X))
& (F = 0.C_Normed_Algebra_of_BoundedFunctions(X) implies ||.F.|| = 0)
& ||.(a*F).|| = (|.a.|)*||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.||)
proof
let X be non empty set, a be Complex,
F, G be Point of C_Normed_Algebra_of_BoundedFunctions(X);
A1:now
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX;
F in ComplexBoundedFunctions(X);
then consider g being Function of X,COMPLEX such that
A2:F = g and
A3:g | X is bounded;
A4:not PreNorms g is empty & PreNorms g is bounded_above by A3,Th14;
consider r0 being set such that
A5:r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A5;
A6:( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:62;
assume F = 0.C_Normed_Algebra_of_BoundedFunctions(X); then
A7: z = g by A2,Th22;
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,FUNCOP_1:13
.= 0;
hence 0 <= r & r <=0 by A9;
end; then
0<=r0 by A5; then
upper_bound (PreNorms g) = 0 by A8,A4,A6,A5,SEQ_4:def 4;
hence ||.F.|| = 0 by A2,A3,Th17;
end;
A10:||.(F + G).|| <= ||.F.|| + ||.G.||
proof
F + G in ComplexBoundedFunctions(X);
then consider h1 being Function of X,COMPLEX such that
A11:h1 = F + G and
A12:h1 | X is bounded;
G in ComplexBoundedFunctions(X);
then consider g1 being Function of X,COMPLEX such that
A13:g1 = G and
A14:g1 | X is bounded;
F in ComplexBoundedFunctions(X);
then consider f1 being Function of X,COMPLEX 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,Th23; then
A18: |. f1.t .| + |. g1.t .| <= ||.F.|| + ||.G.|| by XREAL_1:9;
( |.(h1.t).| = |.(f1.t) + (g1.t).|
& |.(f1.t) + (g1.t).| <= |.(f1.t).| + |.(g1.t).| )
by A15,A13,A11,Th26,COMPLEX1:142;
hence |.(h1.t).| <= ||.F.|| + ||.G.|| by A18,XXREAL_0:2;
end;
A19:now
let r be real number;
assume r in PreNorms h1;
then ex t being Element of X st r = |.(h1.t).|;
hence r <= ||.F.|| + ||.G.|| by A17;
end;
( for s being real number st s in PreNorms h1 holds
s <= ||.F.|| + ||.G.|| ) implies
upper_bound(PreNorms h1) <= ||.F.|| + ||.G.|| by SEQ_4:62;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11,A12,A19,Th17;
end;
A20:||.(a * F).|| = (|.a.|) * ||.F.||
proof
F in ComplexBoundedFunctions(X);
then consider f1 being Function of X,COMPLEX such that
A21: f1 = F and
A22: f1 | X is bounded;
a * F in ComplexBoundedFunctions(X);
then consider h1 being Function of X,COMPLEX 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,Th27; then
|.(h1.t).| = |.a.| * |.(f1.t).| by COMPLEX1:151;
hence |.(h1.t).| <= |.a.| * ||.F.|| by A21,A22,Th23,XREAL_1:66;
end;
A27:now
let r be real number;
assume r in PreNorms h1;
then ex t being Element of X st r = |.(h1.t).|;
hence r <= |.a.| * ||.F.|| by A25;
end;
( ( for s being real number st s in PreNorms h1 holds
s <= |.a.| * ||.F.|| ) implies
upper_bound (PreNorms h1) <= |.a.| * ||.F.|| ) by SEQ_4:62; then
A28: ||.(a * F).|| <= |.a.| * ||.F.|| by A23,A24,A27,Th17;
per cases;
suppose
A29: a <> 0;
A30: now
let t be Element of X;
|.(a " ).| = |.(1 / a).|; then
A31: |.(a " ).| = 1 / |.a.| by COMPLEX1:166;
h1.t = a * (f1.t) by A21,A23,Th27;
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:151;
hence |.(f1.t).| <= ((|.a.|) " ) * ||.(a * F).||
by A23,A24,A32,A31,Th23,XREAL_1:66;
end;
A33: now
let r be Real;
assume r in PreNorms f1;
then ex t being Element of X st r = |.(f1.t).|;
hence r <= ((|.a.|) " ) * ||.(a * F).|| by A30;
end;
( for s being real number st s in PreNorms f1 holds
s <= ((|.a.|) " ) * ||.(a * F).|| ) implies
upper_bound (PreNorms f1) <= ((|.a.|) " ) * ||.(a * F).||
by SEQ_4:62;
then ||.F.|| <= ((|.a.|) " ) * ||.(a * F).|| by A21,A22,A33,Th17;
then |.a.| * ||.F.|| <= |.a.| * (((|.a.|) " ) * ||.(a * F).||)
by XREAL_1:66; then
|.a.| * ||.F.|| <= (|.a.| * ((|.a.|) " )) * ||.(a * F).||;
then |.a.| * ||.F.|| <= 1 * ||.(a * F).|| by A29,XCMPLX_0:def 7;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A28,XXREAL_0:1;
end;
suppose
A35: a = 0;
reconsider fz = F as VECTOR of C_Algebra_of_BoundedFunctions(X);
a * fz = (a + a) * fz by A35
.= (a * fz) + (a * fz) by CLVECT_1:def 3;
then 0.C_Algebra_of_BoundedFunctions(X)
= (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:63;
then 0.C_Algebra_of_BoundedFunctions(X)
= ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def 6;
then 0.C_Algebra_of_BoundedFunctions(X)
= (0.C_Algebra_of_BoundedFunctions(X)) + (a * fz) by VECTSP_1:63;
then
A36: a * F = 0.C_Normed_Algebra_of_BoundedFunctions(X) by RLVECT_1:10;
|.a.| * ||.F.|| = 0 * ||.F.|| by A35;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A36,Th25;
end;
end;
now
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX;
F in ComplexBoundedFunctions(X);
then consider g being Function of X,COMPLEX such that
A37: F = g and
A38: g | X is bounded;
assume
A39:||.F.|| = 0;
now
let t be Element of X;
|.(g.t).| = 0 by A37,A38,A39,Th23;
hence g.t = 0
.= z.t by FUNCOP_1:13;
end;
then g = z by FUNCT_2:113;
hence F = 0.C_Normed_Algebra_of_BoundedFunctions(X) by A37,Th22;
end;
hence thesis by A1,A20,A10;
end;
Th30:
for X being non empty set holds
C_Normed_Algebra_of_BoundedFunctions(X) is
reflexive discerning ComplexNormSpace-like
proof
let X be non empty set;
thus ||.(0.C_Normed_Algebra_of_BoundedFunctions(X)).|| = 0 by Th29;
for x, y being Point of C_Normed_Algebra_of_BoundedFunctions(X)
for a being Complex holds
( ( ||.x.|| = 0 implies x = 0.C_Normed_Algebra_of_BoundedFunctions(X) )
& ( x = 0.C_Normed_Algebra_of_BoundedFunctions(X) implies ||.x.|| = 0 )
& ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
by Th29;
hence thesis by CLVECT_1:def 14,NORMSP_0:def 5;
end;
registration let X be non empty set;
cluster C_Normed_Algebra_of_BoundedFunctions(X) -> right_complementable
Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital discerning
reflexive ComplexNormSpace-like;
coherence by Th21,Th30;
end;
theorem Th31:
for X being non empty set,
f, g, h being Function of X,COMPLEX,
F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(X)
st f = F & g = G & h = H holds
( H = F-G iff for x being Element of X holds h.x = (f.x)-(g.x))
proof
let X be non empty set,
f, g, h be Function of X,COMPLEX,
F, G, H be Point of C_Normed_Algebra_of_BoundedFunctions(X);
assume
A1: f = F & g = G & h = H;
A2:now
assume
A3: for x being 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,Th26;
then F - G = H + (G - G) by RLVECT_1:def 6;
then F - G = H + (0.C_Normed_Algebra_of_BoundedFunctions X)
by RLVECT_1:28;
hence F - G = H by RLVECT_1:10;
end;
now
assume H = F - G;
then H + G = F - (G - G) by RLVECT_1:43;
then H + G = F - (0.C_Normed_Algebra_of_BoundedFunctions X)
by RLVECT_1:28; then
A4: H + G = F by RLVECT_1:26;
now
let x be Element of X;
f.x = (h.x) + (g.x) by A1,A4,Th26;
hence (f.x) - (g.x) = h.x;
end;
hence for x being Element of X holds h.x = (f.x) - (g.x);
end;
hence thesis by A2;
end;
theorem Th32:
for X being non empty set,
seq being sequence of C_Normed_Algebra_of_BoundedFunctions(X)
st seq is CCauchy holds seq is convergent
proof
let X be non empty set,
vseq be sequence of C_Normed_Algebra_of_BoundedFunctions(X);
defpred S1[set, set] means ex xseq being Complex_Sequence st
(for n being Element of NAT holds xseq.n=modetrans(vseq.n,X).$1
& xseq is convergent & $2 = lim xseq );
assume
A1: vseq is CCauchy;
A2:for x being Element of X ex y being Element of COMPLEX st S1[x,y]
proof
let x be Element of X;
deffunc H1( Element of NAT )= modetrans((vseq.$1),X).x;
consider xseq being Complex_Sequence such that
A3: for n being Element of NAT holds xseq.n=H1(n) from FUNCT_2:sch 4;
take y = lim xseq;
A4: for m, k being Element of NAT holds
|.(xseq.m)-(xseq.k).|<=||.((vseq.m)-(vseq.k)).||
proof
let m, k be Element of NAT;
(vseq.m) - (vseq.k) in ComplexBoundedFunctions X;
then consider h1 being Function of X,COMPLEX such that
A5: h1 = (vseq.m) - (vseq.k) and
A6: h1 | X is bounded;
vseq.m in ComplexBoundedFunctions X;
then ex vseqm being Function of X,COMPLEX st
vseq.m = vseqm & vseqm | X is bounded; then
A7: modetrans((vseq.m),X) = vseq.m by Th16;
vseq.k in ComplexBoundedFunctions X;
then ex vseqk being Function of X,COMPLEX st
vseq.k = vseqk & vseqk | X is bounded; then
A8: modetrans ((vseq.k),X) = vseq.k by Th16;
( xseq.m = (modetrans((vseq.m),X)).x
& xseq.k = modetrans( (vseq.k),X).x ) by A3;
then (xseq.m) - (xseq.k) = h1.x by A7,A8,A5,Th31;
hence |.(xseq.m) - (xseq.k).|
<= ||.((vseq.m) - (vseq.k)).|| by A5,A6,Th23;
end;
now
let e be Real;
assume e > 0;
then consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq.n) - (vseq.m)).|| < e by A1,CSSPACE3:10;
take k;
hereby
let n be Element of NAT;
assume n >= k; then
A10: ||.((vseq.n) - (vseq.k)).|| < e by A9;
|.(xseq.n)-(xseq.k).|<=||.((vseq.n)-(vseq.k)).|| by A4;
hence |.(xseq.n) - (xseq.k).| < e by A10,XXREAL_0:2;
end;
end;
then xseq is convergent by COMSEQ_3:46;
hence S1[x,y] by A3;
end;
consider tseq being Function of X,COMPLEX such that
A11: for x being Element of X holds S1[x,(tseq.x)] from FUNCT_2:sch 3(A2);
now
let e1 be real number;
assume
A12: e1 > 0;
reconsider e = e1 as Real by XREAL_0:def 1;
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq.n) - (vseq.m)).|| < e by A1,A12,CSSPACE3:10;
take k;
now
let m be Element of NAT;
A14:||.(vseq.m).|| = ||.vseq.||.m by NORMSP_0:def 4;
assume m >= k;
then
A15:||.((vseq.m) - (vseq.k)).|| < e by A13;
( |.(||.(vseq.m).|| - ||.(vseq.k).||) .|
<= ||.((vseq.m) - (vseq.k)).||
& ||.(vseq.k).|| = ||.vseq.||.k )
by CLVECT_1:111,NORMSP_0:def 4;
hence |.((||.vseq.||.m) - (||.vseq.||.k)).| < e1
by A15,A14,XXREAL_0:2;
end;
hence for m being Element of NAT st m >= k holds
|. ((||.vseq.||.m) - (||.vseq.||.k)) .| < e1;
end; then
A16: ||.vseq.|| is convergent by SEQ_4:58;
now
let x be set;
assume
A17: x in X /\ (dom tseq);
then consider xseq being Complex_Sequence such that
A18: for n being Element of NAT holds xseq.n=modetrans((vseq.n),X).x and
A19: ( xseq is convergent & tseq.x = lim xseq ) by A11;
A20: for n being Element of NAT holds |.xseq.|.n <= ||.vseq.||.n
proof
let n be Element of NAT;
A21: xseq.n = modetrans((vseq.n),X).x by A18;
vseq.n in ComplexBoundedFunctions X; then
A22: ex h1 being Function of X,COMPLEX st
vseq.n = h1 & h1 | X is bounded;
then modetrans((vseq.n),X) = vseq.n by Th16;
then |.(xseq.n).| <= ||.(vseq.n).|| by A17,A22,A21,Th23;
then |.xseq.|.n <= ||.(vseq.n).|| by VALUED_1:18;
hence |.xseq.|.n <= ||.vseq.||.n by NORMSP_0:def 4;
end;
( |.xseq.| is convergent & |.(tseq.x).| = lim (|.xseq.| ))
by A19,COMSEQ_2:11;
hence |.(tseq.x).| <= lim ||.vseq.|| by A16,A20,SEQ_2:32;
end; then
for x be Element of X st x in X /\ (dom tseq) holds
|.tseq /.x.| <= lim ||.vseq.||;
then tseq | X is bounded by CFUNCT_1:81;
then tseq in ComplexBoundedFunctions X;
then reconsider tv = tseq
as Point of C_Normed_Algebra_of_BoundedFunctions(X);
A23:for e being Real st e > 0 holds ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds
|.(modetrans((vseq.n),X).x - (tseq.x)).| <= e
proof
let e be Real;
assume e > 0;
then consider k being Element of NAT such that
A24: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq.n) - (vseq.m)).|| < e by A1,CSSPACE3:10;
take k;
now
let n be Element of NAT;
assume
A25: n >= k;
now
let x be Element of X;
consider xseq being Complex_Sequence such that
A26: for n being Element of NAT
holds xseq.n = modetrans((vseq.n),X).x and
A27: xseq is convergent and
A28: tseq.x = lim xseq by A11;
reconsider fseq = NAT --> (xseq.n) as Complex_Sequence;
set wseq = xseq - fseq;
deffunc H1( Element of NAT ) = |.((xseq.$1) - (xseq.n)).|;
consider rseq being Real_Sequence such that
A29: for m being Element of NAT holds rseq.m = H1(m) from SEQ_1:sch 1;
A30: for m, k being Element of NAT
holds |.((xseq.m) - (xseq.k)).|
<= ||.((vseq.m) - (vseq.k)).||
proof
let m, k be Element of NAT;
(vseq.m) - (vseq.k) in ComplexBoundedFunctions(X);
then consider h1 being Function of X,COMPLEX such that
A31: h1 = (vseq.m) - (vseq.k) and
A32: h1 | X is bounded;
vseq.m in ComplexBoundedFunctions X;
then ex vseqm being Function of X,COMPLEX st
vseq.m = vseqm & vseqm | X is bounded; then
A33: modetrans((vseq.m),X) = vseq.m by Th16;
vseq.k in ComplexBoundedFunctions(X);
then ex vseqk being Function of X,COMPLEX st
vseq.k = vseqk & vseqk | X is bounded; then
A34: modetrans((vseq.k),X) = vseq.k by Th16;
( xseq.m = modetrans((vseq.m),X).x
& xseq.k = modetrans((vseq.k),X).x ) by A26;
then (xseq.m) - (xseq.k) = h1.x by A33,A34,A31,Th31;
hence |.((xseq.m) - (xseq.k)).|
<= ||.((vseq.m) - (vseq.k)).|| by A31,A32,Th23;
end;
A35: for m being Element of NAT st m >= k holds rseq.m <= e
proof
let m be Element of NAT;
assume m >= k; then
A36: ||.((vseq.n) - (vseq.m)).|| < e by A24,A25;
rseq.m = |.((xseq.m) - (xseq.n)).| by A29;
then rseq.m = |.((xseq.n)-(xseq.m)).| by COMPLEX1:146;
then rseq.m <= ||.((vseq.n) - (vseq.m)).|| by A30;
hence rseq.m <= e by A36,XXREAL_0:2;
end;
A37: now
let m be Element of NAT;
(xseq - fseq).m = xseq.m + (-fseq).m by VALUED_1:1
.= xseq.m - fseq.m by VALUED_1:8;
hence (xseq - fseq).m = (xseq.m) - (xseq.n) by FUNCOP_1:13;
end;
now
let x be set;
assume x in NAT;
then reconsider k = x as Element of NAT;
rseq.x = |.((xseq.k) - (xseq.n)).| by A29;
then rseq.x = |.((xseq - fseq).k).| by A37;
hence rseq.x = (|.(xseq - fseq).|).x by VALUED_1:18;
end; then
A38: rseq = |.(xseq - fseq).| by FUNCT_2:18;
A39: fseq is convergent by CFCONT_1:48;
A41: lim rseq <= e by A39,A35,A38,A27,RSSPACE2:6;
lim fseq = fseq.0 by CFCONT_1:50;
then lim fseq = xseq.n by FUNCOP_1:13;
then lim (xseq-fseq)=(tseq.x)-(xseq.n) by A27,A28,A39,COMSEQ_2:26;
then lim rseq = |.((tseq.x)-(xseq.n)).| by A39,A27,A38,COMSEQ_2:11;
then |.((xseq.n)-(tseq.x)).|<= e by A41,COMPLEX1:146;
hence |.(modetrans((vseq.n),X).x - tseq.x).| <= e by A26;
end;
hence for x being Element of X
holds |.(modetrans((vseq.n),X).x-tseq.x).|<= e;
end;
hence for n being Element of NAT st n >= k holds
for x being Element of X
holds |.(modetrans((vseq.n),X).x-tseq.x).|<=e;
end;
A42:for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq.n) - tv).|| <= e
proof
let e be Real;
assume e > 0;
then consider k being Element of NAT such that
A43:for n being Element of NAT st n >= k holds
for x being Element of X holds
|.(modetrans((vseq.n),X).x-tseq.x).|<= e by A23;
take k;
hereby
let n be Element of NAT;
assume
A44: n >= k;
vseq.n in ComplexBoundedFunctions X;
then consider f1 being Function of X,COMPLEX such that
A45: f1 = vseq.n and
f1 | X is bounded;
(vseq.n) - tv in ComplexBoundedFunctions X;
then consider h1 being Function of X,COMPLEX such that
A46: h1 = (vseq.n) - tv and
A47: h1 | X is bounded;
A48: now
let t be Element of X;
modetrans(vseq.n,X) = f1 & h1.t=(f1.t)-(tseq.t)
by A45,A46,DefB7,Th31;
hence |.(h1.t).| <= e by A43,A44;
end;
A49: now
let r be Real;
assume r in PreNorms h1;
then ex t being Element of X st r = |.(h1.t).|;
hence r <= e by A48;
end;
(for s being real number st s in PreNorms h1 holds s<=e) implies
upper_bound (PreNorms h1) <= e by SEQ_4:62;
hence ||.((vseq.n)-tv).||<=e by A46,A47,A49,Th17;
end;
end;
for e being Real st e > 0 holds ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq.n) - tv).|| < e
proof
let e be Real;
assume
A50: e > 0;
consider m being Element of NAT such that
A51:for n being Element of NAT st n >= m holds
||.((vseq.n)-tv).||<= e / 2 by A42,A50;
take m;
A52:e / 2 < e by A50,XREAL_1:218;
hereby let n be Element of NAT;
assume n >= m;
then ||.((vseq.n) - tv).|| <= e / 2 by A51;
hence ||.((vseq.n) - tv).|| < e by A52,XXREAL_0:2;
end;
end;
hence thesis by CLVECT_1:def 16;
end;
registration let X be non empty set;
cluster C_Normed_Algebra_of_BoundedFunctions(X) -> complete;
coherence
proof
for seq being sequence of C_Normed_Algebra_of_BoundedFunctions(X)
st seq is CCauchy holds seq is convergent by Th32;
hence thesis by CLOPBAN1:def 14;
end;
end;
theorem
for X being non empty set holds
C_Normed_Algebra_of_BoundedFunctions(X) is Complex_Banach_Algebra
proof
let X be non empty set;
set B = C_Normed_Algebra_of_BoundedFunctions(X);
reconsider B = C_Normed_Algebra_of_BoundedFunctions(X)
as non empty Normed_Complex_Algebra by Th19;
set X1 = ComplexBoundedFunctions X;
1.B in ComplexBoundedFunctions X;
then consider ONE being Function of X,COMPLEX such that
A1: ONE = 1.B and
A2: ONE | X is bounded;
1.B = 1_C_Algebra_of_BoundedFunctions(X); then
A3: 1. B = X --> 1r by Th12;
for s being set holds (s in PreNorms ONE iff s = 1)
proof
set t = the Element of X;
let s be set;
A4: (X --> 1).t = 1 by FUNCOP_1:13;
hereby
assume s in PreNorms ONE;
then consider t being Element of X such that
A5: s = |.((X --> 1).t).| by A1,A3;
thus s = 1 by A5,COMPLEX1:134,FUNCOP_1:13;
end;
assume s = 1;
hence s in PreNorms ONE by A1,A3,A4,COMPLEX1:134;
end;
then PreNorms ONE = {1} by TARSKI:def 1;
then upper_bound (PreNorms ONE) = 1 by SEQ_4:22; then
A6: ||.(1. B).|| = 1 by A1,A2,Th17;
A7:now
let a be Complex;
let f, g be Element of B;
f in ComplexBoundedFunctions X;
then consider f1 being Function of X,COMPLEX such that
A8: f1 = f and
f1 | X is bounded;
g in ComplexBoundedFunctions X;
then consider g1 being Function of X,COMPLEX such that
A9: g1 = g and
g1 | X is bounded;
a * (f * g) in ComplexBoundedFunctions X;
then consider h3 being Function of X,COMPLEX such that
A10: h3 = a * (f * g) and
h3 | X is bounded;
f * g in ComplexBoundedFunctions X;
then consider h2 being Function of X,COMPLEX such that
A11: h2 = f * g and
h2 | X is bounded;
a * g in ComplexBoundedFunctions X;
then consider h1 being Function of X,COMPLEX such that
A12: h1 = a * g and
h1 | X is bounded;
now
let x be Element of X;
h3.x = a * (h2.x) by A11,A10,Th27;
then h3.x = a * ((f1.x) * (g1.x)) by A8,A9,A11,Th28;
then h3.x = (f1.x) * (a * (g1.x));
hence h3.x = (f1.x) * (h1.x) by A9,A12,Th27;
end;
hence a * (f * g) = f * (a * g) by A8,A12,A10,Th28;
end;
A13:now
let f, g be Element of B;
f in ComplexBoundedFunctions X;
then consider f1 being Function of X,COMPLEX such that
A14: f1 = f and
A15: f1 | X is bounded;
g in ComplexBoundedFunctions X;
then consider g1 being Function of X,COMPLEX such that
A16: g1 = g and
A17: g1 | X is bounded;
A18: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above) by A17,Th13;
f * g in ComplexBoundedFunctions(X);
then consider h1 being Function of X,COMPLEX such that
A19: h1 = f * g and
A20: h1 | X is bounded;
A21: not PreNorms f1 is empty & PreNorms f1 is bounded_above by A15,Th13;
now
let s be real number;
assume s in PreNorms h1;
then consider t being Element of X such that
A22: s = |.(h1.t).|;
|.(g1.t).| in PreNorms g1; then
A23: |.(g1.t).| <= upper_bound (PreNorms g1) by A18,SEQ_4:def 4;
|.(f1.t).| in PreNorms f1; then
A24: |.(f1.t).| <= upper_bound (PreNorms f1) by A21,SEQ_4:def 4; then
A25: (upper_bound (PreNorms f1)) * |.(g1.t).|
<= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by A23,XREAL_1:66;
A26: |.(f1.t).|*|.(g1.t).|<=(upper_bound(PreNorms f1))*|.(g1.t).|
by A24,XREAL_1:66;
|.h1.t.| = |.((f1.t) * (g1.t)).| by A14,A16,A19,Th28;
then abs (h1.t) = |.(f1.t).| * |.(g1.t).| by COMPLEX1:151;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
by A22,A26,A25,XXREAL_0:2;
end;
then
A27:upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) *
(upper_bound PreNorms g1) by SEQ_4:62;
A28: ||.g.|| = upper_bound PreNorms g1 by A16,A17,Th17;
||.f.|| = upper_bound PreNorms f1 by A14,A15,Th17;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A19,A20,A28,A27,Th17;
end;
A29:now
let f, g, h be Element of B;
f in ComplexBoundedFunctions X;
then consider f1 being Function of X,COMPLEX such that
A30: f1 = f and
f1 | X is bounded;
h in ComplexBoundedFunctions X;
then consider h1 being Function of X,COMPLEX such that
A31: h1 = h and
h1 | X is bounded;
g in ComplexBoundedFunctions X;
then consider g1 being Function of X,COMPLEX such that
A32: g1 = g and
g1 | X is bounded;
(g + h) * f in ComplexBoundedFunctions X;
then consider F1 being Function of X,COMPLEX such that
A33:F1 = (g + h) * f and
F1 | X is bounded;
h * f in ComplexBoundedFunctions X;
then consider hf1 being Function of X,COMPLEX such that
A34: hf1 = h * f and
hf1 | X is bounded;
g * f in ComplexBoundedFunctions X;
then consider gf1 being Function of X,COMPLEX such that
A35: gf1 = g * f and
gf1 | X is bounded;
g + h in ComplexBoundedFunctions X;
then consider gPh1 being Function of X,COMPLEX such that
A36: gPh1 = g + h and
gPh1 | X is bounded;
now
let x be Element of X;
F1.x = (gPh1.x) * (f1.x) by A30,A36,A33,Th28;
then F1.x = ((g1.x) + (h1.x)) * (f1.x) by A32,A31,A36,Th26;
then F1.x = ((g1.x) * (f1.x)) + ((h1.x) * (f1.x));
then F1.x = (gf1.x) + ((h1.x) * (f1.x)) by A30,A32,A35,Th28;
hence F1.x = (gf1.x) + (hf1.x) by A30,A31,A34,Th28;
end;
hence (g + h) * f = (g * f) + (h * f) by A35,A34,A33,Th26;
end;
for f being Element of B holds (1. B) * f = f by Lm2; then
A37:B is left_unital by VECTSP_1:def 19;
A38:B is Banach_Algebra-like_1 by A13,CLOPBAN2:def 9;
A39:B is Banach_Algebra-like_2 by A6,CLOPBAN2:def 10;
A40:B is Banach_Algebra-like_3 by A7,CLOPBAN2:def 11;
B is left-distributive by A29,VECTSP_1:def 12;
hence thesis by A37,A38,A39,A40;
end;