:: Banach Algebra of Continuous Functionals and Space of Real-valued :: Continuous Functionals with Bounded Support :: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama :: :: Received October 20, 2009 :: Copyright (c) 2009-2012 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, PSCOMP_1, NUMBERS, PRE_TOPC, ORDINAL2, SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3, XXREAL_1, ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, POLYALG1, BINOP_1, VECTSP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, RSSPACE4, XXREAL_2, XXREAL_0, LOPBAN_2, NORMSP_1, REWRITE1, NAT_1, RSSPACE3, SEQ_2, PARTFUN1, SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1, TOPMETR; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, REALSET1, FUNCT_1, FUNCT_2, STRUCT_0, ALGSTR_0, IDEAL_1, BINOP_1, DOMAIN_1, RELSET_1, PRE_TOPC, COMPTS_1, PSCOMP_1, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, PARTFUN1, SEQFUNC, RSSPACE3, RCOMP_1, SEQ_2, NORMSP_0, NORMSP_1, NFCONT_1, LOPBAN_1, LOPBAN_2, C0SP1, CONNSP_2, FUNCOP_1, PRE_POLY, XXREAL_2, VALUED_1, RLSUB_1, RSSPACE, TOPMETR; constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, SEQ_1, C0SP1, NFCONT_1, SEQFUNC, MEASURE6, PRE_POLY, TOPMETR, RLSUB_1, SEQ_4, NAGATA_1, PSCOMP_1, COMPTS_1, COMSEQ_2; registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, VECTSP_1, VECTSP_2, VALUED_0, LOPBAN_2, PSCOMP_1, RCOMP_1, C0SP1, COMPTS_1, XXREAL_0, FUNCT_2, VALUED_1, XXREAL_2, TOPMETR, RELSET_1, WAYBEL_2, JORDAN5A; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions PSCOMP_1, REALSET1, ALGSTR_0, TARSKI, XCMPLX_0, RCOMP_1, FUNCSDOM, RLVECT_1, VECTSP_1, STRUCT_0, GROUP_1, BINOP_1, C0SP1, NORMSP_0; theorems RFUNCT_1, FUNCT_1, NFCONT_1, PARTFUN1, SEQ_2, ABSVALUE, ALGSTR_0, COMPLEX1, ZFMISC_1, TARSKI, RCOMP_1, XBOOLE_1, PSCOMP_1, IDEAL_1, RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1, FUNCT_2, XREAL_1, RLVECT_1, TOPS_1, FUNCOP_1, VECTSP_1, GROUP_1, LOPBAN_2, VALUED_1, C0SP1, CONNSP_2, XXREAL_1, NORMSP_0, PRE_POLY, XBOOLE_0, RSSPACE, COMPTS_1, PRE_TOPC, RLSUB_1, JORDAN_A, NAGATA_1, JGRAPH_2, TOPMETR, JORDAN5A, XXREAL_2; begin :: Banach Algebra of Continuous Functionals definition let X be 1-sorted, y be real number; func X --> y -> RealMap of X equals (the carrier of X) --> y; coherence proof y in REAL by XREAL_0:def 1; then (the carrier of X) --> y is RealMap of X by FUNCOP_1:45; hence thesis; end; end; registration let X be TopSpace, y be real number; cluster X --> y -> continuous; coherence proof set f = X --> y; set HX=[#] X; let P1 be Subset of REAL such that P1 is closed; per cases; suppose y in P1; then f"P1 = HX by FUNCOP_1:14; hence f"P1 is closed; end; suppose not y in P1; then f"P1 = {}X by FUNCOP_1:16; hence f"P1 is closed; end; end; end; theorem Th1: for X being non empty TopSpace, f be RealMap of X holds f is continuous iff for x being Point of X,V being Subset of REAL st f.x in V & V is open holds ex W being Subset of X st x in W & W is open & f.:W c= V proof let X be non empty TopSpace,f be RealMap of X; hereby assume A1: f is continuous; now let x be Point of X,V being Subset of REAL; set r = f.x; assume r in V & V is open; then consider r0 be real number such that A2: 0 Subset of RAlgebra the carrier of X equals { f where f is continuous RealMap of X : not contradiction }; correctness proof set A = { f where f is continuous RealMap of X : not contradiction }; A c= Funcs(the carrier of X,REAL) proof let x be set; assume x in A; then ex f be continuous RealMap of X st x=f; hence x in Funcs(the carrier of X,REAL) by FUNCT_2:8; end; hence thesis; end; end; registration let X be non empty TopSpace; cluster ContinuousFunctions(X) -> non empty; coherence proof X-->0 in { f where f is continuous RealMap of X : not contradiction }; hence thesis; end; end; registration let X be non empty TopSpace; cluster ContinuousFunctions(X) -> additively-linearly-closed multiplicatively-closed; coherence proof set W = ContinuousFunctions(X); set V = RAlgebra the carrier of X; A1:RAlgebra the carrier of X is RealLinearSpace by C0SP1:7; 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 continuous RealMap of X such that A3: v1=v by A2; consider u1 be continuous RealMap of X such that A4: u1=u by A2; A5: v1+u1 is Function of the carrier of X,REAL & v1+u1 is continuous by NAGATA_1:22; reconsider h = v+u as Element of Funcs(the carrier of X,REAL); A6: ex f being Function st h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2; dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then A7: dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of 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,FUNCSDOM: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 continuous RealMap of X such that A10: v1=v by A9; A11:-v1 is continuous RealMap of X by PSCOMP_1:9; reconsider h = -v, v2 = v as Element of Funcs(the carrier of X,REAL); A12:h=(-1)*v by A1,RLVECT_1:16; A13:ex f being Function st h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2; A14:dom v1 =the carrier of X by FUNCT_2:def 1; now let x be set; assume x in dom h; then reconsider y=x as Element of the carrier of X; h.x = (-1)*(v2.y) by A12,FUNCSDOM:4; 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 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 A16: u in W; consider u1 be continuous RealMap of X such that A17: u1=u by A16; A18:a(#)u1 is continuous RealMap of X proof reconsider U = u1 as continuous Function of X,R^1 by JORDAN5A:27,TOPMETR:17; set c = the carrier of X; consider H being Function of X,R^1 such that A19: for p being Point of X for r1 being real number st U . p = r1 holds H . p = a * r1 and A20: H is continuous by JGRAPH_2:23; reconsider h = H as RealMap of X by TOPMETR:17; A21: dom h = the carrier of X by FUNCT_2:def 1 .= dom u1 by FUNCT_2:def 1; for c being set st c in dom h holds h . c = a * (u1 . c) by A19; then h = a (#) u1 by A21,VALUED_1:def 5; hence a (#) u1 is continuous RealMap of X by A20,JORDAN5A:27; end; reconsider h = a*u as Element of Funcs(the carrier of X,REAL); A22:ex f being Function st h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2; A23:dom u1 = the carrier of X by FUNCT_2:def 1; for x be set st x in dom h holds h.x = a*(u1.x) by A17,FUNCSDOM:4; then a*u=a(#)u1 by A23,A22,VALUED_1:def 5; hence a*u in W by A18; end; hence ContinuousFunctions(X) is additively-linearly-closed by A8,A15,C0SP1:def 10; A24: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 A25: v in W & u in W; consider v1 be continuous RealMap of X such that A26: v1=v by A25; consider u1 be continuous RealMap of X such that A27: u1=u by A25; A28:v1(#)u1 is continuous RealMap of X proof reconsider V = v1, U = u1 as continuous Function of X,R^1 by JORDAN5A:27,TOPMETR:17; consider H being Function of X,R^1 such that A29: for p being Point of X for r1, r2 being real number st V . p = r1 & U . p = r2 holds H . p = r1 * r2 and A30: H is continuous by JGRAPH_2:25; reconsider h = H as RealMap of X by TOPMETR:17; A31: dom h = (the carrier of X) /\ (the carrier of X) by FUNCT_2:def 1 .= (the carrier of X) /\ (dom u1) by FUNCT_2:def 1 .= (dom v1) /\ (dom u1) by FUNCT_2:def 1; for c being set st c in dom h holds h . c = (v1 . c) * (u1 . c) by A29; then h = v1 (#) u1 by A31,VALUED_1:def 4; hence v1 (#) u1 is continuous RealMap of X by A30,JORDAN5A:27; end; reconsider h = v*u as Element of Funcs(the carrier of X,REAL); A32:ex f being Function st h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2; dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then A33:dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of X) by FUNCT_2:def 1; for x be set st x in dom h holds h.x = v1.x *u1.x by A26,A27,FUNCSDOM:2; then v*u=v1(#)u1 by A33,A32,VALUED_1:def 4; hence v*u in W by A28; end; reconsider g = RealFuncUnit the carrier of X as RealMap of X; g = X --> 1; then 1.V in W; hence thesis by A24,C0SP1:def 4; end; end; definition let X be non empty TopSpace; func R_Algebra_of_ContinuousFunctions(X) -> AlgebraStr equals AlgebraStr (# ContinuousFunctions(X), mult_(ContinuousFunctions(X),RAlgebra the carrier of X), Add_(ContinuousFunctions(X),RAlgebra the carrier of X), Mult_(ContinuousFunctions(X),RAlgebra the carrier of X), One_(ContinuousFunctions(X),RAlgebra the carrier of X), Zero_(ContinuousFunctions(X),RAlgebra the carrier of X) #); coherence; end; theorem for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; registration let X be non empty TopSpace; cluster R_Algebra_of_ContinuousFunctions(X) -> strict non empty; coherence; end; registration let X be non empty TopSpace; cluster R_Algebra_of_ContinuousFunctions(X) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative; coherence proof now let v be VECTOR of R_Algebra_of_ContinuousFunctions(X); reconsider v1=v as VECTOR of RAlgebra the carrier of X by TARSKI:def 3; R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; then 1 * v = 1*v1 by C0SP1:8; hence 1 * v =v by FUNCSDOM:12; end; hence thesis by C0SP1:6,RLVECT_1:def 8; end; end; theorem Th3: for X being non empty TopSpace for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X) for f,g,h being RealMap of X holds (f=F & g=G & h=H implies ( H = F+G iff (for x be Element of the carrier of X holds h.x = f.x + g.x))) proof let X be non empty TopSpace; let F,G,H be VECTOR of R_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; assume A1: f=F & g=G & h=H; A2:R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra the carrier of X by TARSKI:def 3; hereby assume A3: H = F+G; let x be Element of the carrier of X; h1=f1+g1 by A2,A3,C0SP1:8; hence h.x = f.x+g.x by A1,FUNCSDOM:1; end; assume for x be Element of X holds h.x = f.x+g.x; then h1=f1+g1 by A1,FUNCSDOM:1; hence H =F+G by A2,C0SP1:8; end; theorem Th4: for X being non empty TopSpace for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X) for f,g,h being RealMap of X for a being Real holds (f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )) proof let X be non empty TopSpace; let F,G,H be VECTOR of R_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; let a be Real; assume A1: f=F & g=G; A2:R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; reconsider f1=F, g1=G as VECTOR of RAlgebra the carrier of X by TARSKI:def 3; hereby assume A3: G = a*F; let x be Element of the carrier of X; g1=a*f1 by A2,A3,C0SP1:8; hence g.x=a*f.x by A1,FUNCSDOM:4; end; assume for x be Element of the carrier of X holds g.x=a*f.x; then g1=a*f1 by A1,FUNCSDOM:4; hence G =a*F by A2,C0SP1:8; end; theorem Th5: for X being non empty TopSpace for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X) for f,g,h being RealMap of X holds (f=F & g=G & h=H implies ( H = F*G iff (for x be Element of the carrier of X holds h.x = f.x * g.x))) proof let X be non empty TopSpace; let F,G,H be VECTOR of R_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; assume A1: f=F & g=G & h=H; A2:R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra the carrier of X by TARSKI:def 3; hereby assume A3: H = F*G; let x be Element of the carrier of X; h1 = f1*g1 by A2,A3,C0SP1:8; hence h.x = f.x * g.x by A1,FUNCSDOM:2; end; assume for x be Element of X holds h.x = f.x * g.x; then h1 = f1 * g1 by A1,FUNCSDOM:2; hence H = F * G by A2,C0SP1:8; end; theorem Th6: for X being non empty TopSpace holds 0.R_Algebra_of_ContinuousFunctions(X) = X --> 0 proof let X be non empty TopSpace; A1:R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; 0.RAlgebra the carrier of X = X --> 0; hence thesis by A1,C0SP1:8; end; theorem Th7: for X being non empty TopSpace holds 1_R_Algebra_of_ContinuousFunctions(X) = X --> 1 proof let X be non empty TopSpace; A1:R_Algebra_of_ContinuousFunctions(X) is Subalgebra of RAlgebra the carrier of X by C0SP1:6; 1_RAlgebra the carrier of X = X --> 1; hence thesis by A1,C0SP1:8; end; theorem Th8: for A being Algebra, A1,A2 being Subalgebra of A holds the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2 proof let A be Algebra, A1,A2 be Subalgebra of A; assume A1: the carrier of A1 c= the carrier of A2; set CA1 = the carrier of A1; set CA2 = the carrier of A2; set AA = the addF of A; set mA = the multF of A; set MA = the Mult of A; A2:0.A1 = 0.A & 0.A2 = 0.A & 1.A1 = 1.A & 1.A2 = 1.A by C0SP1:def 9; A3:the addF of A1 = (the addF of A2)||the carrier of A1 proof the addF of A1 = AA||CA1 & the addF of A2 = AA||CA2 & [:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96; hence thesis by FUNCT_1:51; end; A4:the multF of A1 = (the multF of A2)||the carrier of A1 proof the multF of A1 = mA||CA1 & the multF of A2 = mA||CA2 & [:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96; hence thesis by FUNCT_1:51; end; the Mult of A1 = (the Mult of A2) | [:REAL,CA1:] proof the Mult of A1 = MA|[:REAL,CA1:] & the Mult of A2 = MA|[:REAL,CA2:] & [:REAL,CA1:] c= [:REAL,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96; hence thesis by FUNCT_1:51; end; hence thesis by A1,A2,A3,A4,C0SP1:def 9; end; Lm1: for X being compact non empty TopSpace for x being set st x in ContinuousFunctions(X) holds x in BoundedFunctions the carrier of X proof let X be compact non empty TopSpace; let x be set; assume x in ContinuousFunctions(X); then consider h be continuous RealMap of X such that A1: x=h; A2:h is bounded_above & h is bounded_below by SEQ_2:def 8; then consider r1 being real number such that A3: for y being set st y in dom h holds h.y < r1 by SEQ_2:def 1; A4:(the carrier of X) /\ dom h c= dom h by XBOOLE_1:17; then for y being set st y in (the carrier of X) /\ dom h holds h.y<=r1 by A3; then A5:h|(the carrier of X) is bounded_above by RFUNCT_1:70; consider r2 being real number such that A6:for y being set st y in dom h holds r2 Function of (ContinuousFunctions(X)),REAL equals (BoundedFunctionsNorm the carrier of X)|(ContinuousFunctions(X)); correctness proof for x being set st x in ContinuousFunctions(X) holds x in BoundedFunctions the carrier of X by Lm1; then ContinuousFunctions(X) c= BoundedFunctions the carrier of X by TARSKI:def 3; hence thesis by FUNCT_2:32; end; end; definition let X be compact non empty TopSpace; func R_Normed_Algebra_of_ContinuousFunctions(X) -> Normed_AlgebraStr equals Normed_AlgebraStr (# ContinuousFunctions(X), mult_(ContinuousFunctions(X),RAlgebra the carrier of X), Add_(ContinuousFunctions(X),RAlgebra the carrier of X), Mult_(ContinuousFunctions(X),RAlgebra the carrier of X), One_(ContinuousFunctions(X),RAlgebra the carrier of X), Zero_(ContinuousFunctions(X),RAlgebra the carrier of X), ContinuousFunctionsNorm(X) #); correctness; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> strict non empty; correctness; end; Lm2: now let X be compact non empty TopSpace; set F = R_Normed_Algebra_of_ContinuousFunctions(X); let x,e be Element of F; assume A1: e = One_(ContinuousFunctions(X),RAlgebra the carrier of X); set X1 = ContinuousFunctions(X); reconsider f = x as Element of X1; 1_RAlgebra the carrier of X = X-->1 .= 1_R_Algebra_of_ContinuousFunctions(X) by Th7; then A2:[f,1_RAlgebra the carrier of X] in [:X1,X1:] & [1_RAlgebra the carrier of X,f] in [:X1,X1:] by ZFMISC_1:87; x * e = (mult_(X1,RAlgebra the carrier of X)) .(f,1_RAlgebra the carrier of X) by A1,C0SP1:def 8; then x * e = ((the multF of RAlgebra the carrier of X)||X1) .(f,1_RAlgebra the carrier of X) by C0SP1:def 6; then x * e = f * 1_RAlgebra the carrier of X by A2,FUNCT_1:49; hence x * e = x by VECTSP_1:def 4; e * x = (mult_(X1,RAlgebra the carrier of X)) .(1_RAlgebra the carrier of X,f) by A1,C0SP1:def 8; then e * x = ((the multF of RAlgebra the carrier of X)||X1) .(1_RAlgebra the carrier of X,f) by C0SP1:def 6; then e * x = (1_RAlgebra the carrier of X )* f by A2,FUNCT_1:49; hence e * x = x by VECTSP_1:def 4; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> unital; correctness proof reconsider e = One_(ContinuousFunctions(X), RAlgebra the carrier of X) as Element of R_Normed_Algebra_of_ContinuousFunctions(X); take e; thus thesis by Lm2; end; end; theorem Th10: for W be Normed_AlgebraStr, V be Algebra st the AlgebraStr of W = V holds W is Algebra proof let W be Normed_AlgebraStr,V be Algebra such that A1: the AlgebraStr of W = V; reconsider W as non empty AlgebraStr by A1; A2: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; A3:for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z) proof let x,y,z be VECTOR of W; reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1; (x + y) + z = (x1 + y1) + z1 by A1; then (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 3; hence (x + y) + z = x + (y + z) by A1; end; A4:for x being VECTOR of W holds x + 0.W = x proof let x be VECTOR of W; reconsider y = x as VECTOR of V by A1; x + 0.W = y + 0.V by A1; hence x + 0.W = x by RLVECT_1:4; end; A5: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 A6: x1 + v = 0.V by ALGSTR_0:def 11; reconsider y = v as Element of W by A1; x + y = 0.W by A6,A1; hence thesis by ALGSTR_0:def 11; 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 a,b,x being Element of W holds (a * b) * x = a * (b * x) proof let a,b,x be Element of W; reconsider y = x, a1 = a, b1 = b as Element of V by A1; (a * b) * x = (a1 * b1) * y by A1; then (a * b) * x = a1 * (b1 * y) by GROUP_1:def 3; hence (a * b) * x = a * (b * x) by A1; end; A9: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 4; end; A10:W is right-distributive proof let x,y,z being Element of W; reconsider x1 = x, y1 = y, z1 = z as Element of V by A1; x*(y+z) = x1*(y1+z1) by A1; then x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 2; hence x*(y+z) = x*y + x*z by A1; end; W is vector-distributive scalar-distributive scalar-associative vector-associative proof thus W is vector-distributive proof let a be real number; let x,y be Element of W; reconsider x1 = x, y1 = y as Element of V by A1; a*(x+y) = a*(x1+y1) by A1; then a*(x+y) = a*x1 + a*y1 by RLVECT_1:def 5; hence a*(x+y) = a*x + a*y by A1; end; thus W is scalar-distributive proof let a,b be real number; let x be Element of W; reconsider x1 = x as Element of V by A1; (a+b)*x = (a+b)*x1 by A1; then (a+b)*x = a*x1 + b*x1 by RLVECT_1:def 6; hence (a+b)*x =a*x + b*x by A1; end; thus W is scalar-associative proof let a,b be real number; let x being Element of W; reconsider x1 = x as Element of V by A1; (a*b)*x = (a*b)*x1 by A1; then (a*b)*x = a*(b*x1) by RLVECT_1:def 7; hence (a*b)*x = a*(b*x) by A1; end; let x,y be Element of W; let a be Real; 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)*y1 by FUNCSDOM:def 9; hence a*(x*y) = (a*x)*y by A1; end; hence thesis by A2,A3,A4,A5,A7,A8,A9,A10,ALGSTR_0:def 16,GROUP_1:def 3,def 12 ,RLVECT_1:def 2,def 3,def 4; end; Lm3: for X being compact non empty TopSpace for x be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x=y holds ||.x.||= ||.y.|| by FUNCT_1:49; Lm4: for X being compact non empty TopSpace for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x1=y1 & x2=y2 holds x1+x2=y1+y2 proof let X be compact non empty TopSpace; let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x1=y1 & x2=y2; thus x1+x2 = ((the addF of RAlgebra the carrier of X) ||(ContinuousFunctions(X))).([x1,x2]) by C0SP1:def 5 .= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49 .= ((the addF of RAlgebra the carrier of X) ||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49 .=y1+y2 by C0SP1:def 5; end; Lm5: for X being compact non empty TopSpace for a be Real,x be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x=y holds a*x=a*y proof let X be compact non empty TopSpace; let a be Real, x be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x=y; thus a*x = ((the Mult of RAlgebra the carrier of X)| [:REAL,(ContinuousFunctions(X)):]).([a,x]) by C0SP1:def 11 .= (the Mult of RAlgebra the carrier of X).([a,x]) by FUNCT_1:49 .= ((the Mult of RAlgebra the carrier of X) |[:REAL,(BoundedFunctions the carrier of X):]).([a,y]) by A1,FUNCT_1:49 .=a*y by C0SP1:def 11; end; Lm6: for X be compact non empty TopSpace for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x1=y1 & x2=y2 holds x1*x2=y1*y2 proof let X be compact non empty TopSpace; let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x1=y1 & x2=y2; thus x1*x2 = ((the multF of RAlgebra the carrier of X)|| (ContinuousFunctions(X))).([x1,x2]) by C0SP1:def 6 .= (the multF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49 .= ((the multF of RAlgebra the carrier of X) ||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49 .=y1*y2 by C0SP1:def 6; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative; coherence proof 1.(R_Normed_Algebra_of_ContinuousFunctions(X)) = 1_R_Algebra_of_ContinuousFunctions(X); hence thesis by Th10; end; end; theorem Th11: for X being compact non empty TopSpace for F being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds (Mult_(ContinuousFunctions(X), RAlgebra the carrier of X)).(1,F) = F proof let X be compact non empty TopSpace; let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X); set X1 = ContinuousFunctions(X); reconsider f1 = F as Element of X1; A1:[1,f1] in [:REAL,X1:] by ZFMISC_1:87; thus (Mult_(ContinuousFunctions(X), RAlgebra the carrier of X)).(1,F) = ((the Mult of RAlgebra the carrier of X)| [:REAL,X1:]).(1,f1) by C0SP1:def 11 .= (the Mult of RAlgebra the carrier of X).(1,f1) by A1,FUNCT_1:49 .= F by FUNCSDOM:12; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> vector-distributive scalar-distributive scalar-associative scalar-unital; coherence proof for v being VECTOR of R_Normed_Algebra_of_ContinuousFunctions(X) holds 1 * v = v by Th11; hence thesis by RLVECT_1:def 8; end; end; theorem Th12: for X being compact non empty TopSpace holds X --> 0 = 0.R_Normed_Algebra_of_ContinuousFunctions(X) proof let X be compact non empty TopSpace; X-->0 = 0.R_Algebra_of_ContinuousFunctions(X) by Th6; hence thesis; end; Lm7: for X being compact non empty TopSpace holds 0.R_Normed_Algebra_of_ContinuousFunctions(X) = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X proof let X be compact non empty TopSpace; thus 0.R_Normed_Algebra_of_ContinuousFunctions(X) = X-->0 by Th12 .= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:25; end; Lm8: for X being compact non empty TopSpace holds 1.R_Normed_Algebra_of_ContinuousFunctions(X) = 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X proof let X be compact non empty TopSpace; thus 1.R_Normed_Algebra_of_ContinuousFunctions(X) =1_R_Algebra_of_ContinuousFunctions(X) .= X-->1 by Th7 .= 1_R_Algebra_of_BoundedFunctions the carrier of X by C0SP1:16 .= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X; end; theorem for X be compact non empty TopSpace for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds 0 <= ||.F.|| proof let X be compact non empty TopSpace; let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X); reconsider F1=F as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; ||.F.|| =||.F1.|| by FUNCT_1:49; hence thesis by C0SP1:27; end; theorem for X being compact non empty TopSpace for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds F = 0.R_Normed_Algebra_of_ContinuousFunctions(X) implies 0 = ||.F.|| proof let X be compact non empty TopSpace; let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X); assume A1: F = 0.R_Normed_Algebra_of_ContinuousFunctions(X); reconsider F1=F as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; A2:||.F.|| =||.F1.|| by FUNCT_1:49; F= X--> 0 by A1,Th12; then F1 = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:25; hence thesis by A2,C0SP1:28; end; theorem Th15: for X being compact non empty TopSpace for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X) for f,g,h be RealMap of X holds (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 let X be compact non empty TopSpace; let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions(X); H=F+G iff h1=f1+g1; hence thesis by Th3; end; theorem for a be Real for X being compact non empty TopSpace for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X) for f,g being RealMap of X holds (f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )) proof let a be Real; let X be compact non empty TopSpace; let F,G be Point of R_Normed_Algebra_of_ContinuousFunctions(X); let f,g be RealMap of X; reconsider f1=F, g1=G as VECTOR of R_Algebra_of_ContinuousFunctions(X); G=a*F iff g1=a*f1; hence thesis by Th4; end; theorem for X being compact non empty TopSpace for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X) for f,g,h being RealMap of X holds (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 let X be compact non empty TopSpace; let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions(X); H=F*G iff h1=f1*g1; hence thesis by Th5; end; theorem Th18: for a being Real for X being compact non empty TopSpace for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds ( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions(X)) & (||.a*F.|| = abs a * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||) proof let a be Real; let X be compact non empty TopSpace; let F,G be Point of R_Normed_Algebra_of_ContinuousFunctions(X); reconsider F1=F, G1=G as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; A1:||.F.|| =||.F1.|| by FUNCT_1:49; A2:||.G.|| =||.G1.|| by FUNCT_1:49; A3:||.F+G.|| =||.F1+G1.|| by Lm4,Lm3; ||.F1.|| = 0 iff F1=0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:32; hence ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions(X) by Lm7,FUNCT_1:49; thus ||.a*F.|| = ||.a*F1.|| by Lm5,Lm3 .=abs a * ||.F1.|| by C0SP1:32 .=abs a * ||.F.|| by FUNCT_1:49; thus ||.F+G.|| <= ||.F.|| + ||.G.|| by A1,A2,A3,C0SP1:32; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> reflexive discerning RealNormSpace-like; coherence proof set R = R_Normed_Algebra_of_ContinuousFunctions(X); thus ||.0.R.|| = 0 by Th18; for x,y being Point of R_Normed_Algebra_of_ContinuousFunctions(X) for a be Real holds ( ||.x.|| = 0 iff x = 0.R_Normed_Algebra_of_ContinuousFunctions(X) ) & ||.a*x.|| = abs(a) * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th18; hence thesis by NORMSP_0:def 5,NORMSP_1:def 1; end; end; Lm9: for X be compact non empty TopSpace for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x1=y1 & x2=y2 holds x1-x2=y1-y2 proof let X be compact non empty TopSpace; let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x1=y1 & x2=y2; -x2=(-1)*x2 by RLVECT_1:16 .=(-1)*y2 by A1,Lm5 .= -y2 by RLVECT_1:16; hence x1-x2 =y1-y2 by A1,Lm4; end; theorem for X be compact non empty TopSpace for F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X) for f,g,h be RealMap of X holds 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 let X be compact non empty TopSpace; let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X); let f,g,h be RealMap of X; assume A1: f=F & g=G & h=H; A2:now assume H=F-G; then H+G=F-(G-G) by RLVECT_1:29; then H+G=F-0.R_Normed_Algebra_of_ContinuousFunctions(X) by RLVECT_1:15; then A3: H+G=F by RLVECT_1:13; now let x be Element of X; f.x=h.x + g.x by A1,A3,Th15; 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 A4: 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 A4; hence h.x + g.x= f.x; end; then F=H+G by A1,Th15; then F-G=H+(G-G) by RLVECT_1:def 3; then F-G=H+0.R_Normed_Algebra_of_ContinuousFunctions(X) by RLVECT_1:15; hence F-G=H by RLVECT_1:4; end; hence thesis by A2; end; theorem Th20: for X be RealBanachSpace, Y be Subset of X, seq be sequence of X st Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds seq is convergent & lim seq in Y proof let X be RealBanachSpace, Y be Subset of X, seq be sequence of X; assume A1: Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm; hence seq is convergent by LOPBAN_1:def 15; hence thesis by A1,NFCONT_1:def 3; end; theorem Th21: for X be compact non empty TopSpace for Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X st Y = ContinuousFunctions(X) holds Y is closed proof let X be compact non empty TopSpace; let Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: Y = ContinuousFunctions(X); now let seq be sequence of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A2: rng seq c= Y & seq is convergent; lim seq in BoundedFunctions the carrier of X; then consider f be Function of (the carrier of X),REAL such that A3: f=lim seq & f|(the carrier of X) is bounded; now let z be set; assume z in BoundedFunctions (the carrier of X); then ex f be RealMap of X st f=z & f|(the carrier of X) is bounded; hence z in PFuncs(the carrier of X,REAL) by PARTFUN1:45; end; then BoundedFunctions (the carrier of X) c= PFuncs(the carrier of X,REAL) by TARSKI:def 3; then reconsider H = seq as Functional_Sequence of (the carrier of X),REAL by FUNCT_2:7; A4: for p be Real st p>0 ex k be Element of NAT st for n be Element of NAT, x be set st n>=k & x in the carrier of X holds abs((H.n).x - f.x) < p proof let p be Real; assume p>0; then consider k be Element of NAT such that A5: for n be Element of NAT st n >= k holds ||.seq.n - lim seq.|| < p by A2,NORMSP_1:def 7; take k; hereby let n be Element of NAT, x be set; assume A6: n>=k & x in the carrier of X; then A7: ||.seq.n - lim seq.|| < p by A5; seq.n - lim seq in BoundedFunctions the carrier of X; then consider g be RealMap of X such that A8: g=seq.n - lim seq & g|(the carrier of X) is bounded; seq.n in BoundedFunctions the carrier of X; then consider s be RealMap of X such that A9: s=seq.n & s|(the carrier of X) is bounded; reconsider x0 = x as Element of the carrier of X by A6; A10: g.x0= s.x0-f.x0 by A8,A9,A3,C0SP1:34; abs(g.x0) <= ||.seq.n - lim seq.|| by A8,C0SP1:26; hence abs((H.n).x - f.x) < p by A10,A9,A7,XXREAL_0:2; end; end; f is continuous proof for x being Point of X,V being Subset of REAL st f.x in V & V is open holds ex W being Subset of X st x in W & W is open & f.:W c= V proof let x be Point of X,V be Subset of REAL; set r=f.x; assume f.x in V & V is open; then consider r0 being real number such that A11: 0=k & x in the carrier of X holds abs((H.n).x - f.x) < r0/3 by A4,A11,XREAL_1:222; A13: abs((H.k).x - f.x) < r0/3 by A12; k in NAT; then k in dom seq by NORMSP_1:12; then H.k in rng seq by FUNCT_1:def 3; then H.k in Y by A2; then consider h be continuous RealMap of X such that A14: H.k=h by A1; set r1 = h.x; set G1 = ]. r1-r0/3,r1+r0/3 .[; A15: r10; consider k be Element of NAT such that A4: for n,m be Element of NAT st n >= k & m >= k holds ||. vseq.n - vseq.m .|| < e by A1,A3,RSSPACE3:8; take k; now let n,m be Element of NAT; assume n >= k & m >= k; then ||. vseq.n - vseq.m .|| < e by A4; hence ||. vseq1.n - vseq1.m .|| < e by Lm9,Lm3; end; hence for n,m be Element of NAT st n >= k & m >= k holds ||. vseq1.n - vseq1.m .|| < e; end; then A5:vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8; then A6: vseq1 is convergent by C0SP1:35; reconsider Y = ContinuousFunctions(X) as Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X by A2,TARSKI:def 3; A7:rng vseq c= ContinuousFunctions(X); Y is closed by Th21; then reconsider tv=lim vseq1 as Point of R_Normed_Algebra_of_ContinuousFunctions(X) by A7,A5,Th20; for e be Real st e > 0 ex k be Element of NAT st for n be Element of NAT st n >= k holds ||.vseq.n - tv.|| < e proof let e be Real; assume e > 0; then consider k be Element of NAT such that A8: for n be Element of NAT st n >= k holds ||.vseq1.n - lim vseq1.|| < e by A6,NORMSP_1:def 7; take k; now let n be Element of NAT; assume n >= k; then ||.vseq1.n-lim vseq1.|| < e by A8; hence ||.vseq.n-tv.|| < e by Lm9,Lm3; end; hence for n be Element of NAT st n >= k holds ||.vseq.n - tv.|| < e; end; hence thesis by NORMSP_1:def 6; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> complete; coherence proof for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions(X) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th22; hence thesis by LOPBAN_1:def 15; end; end; registration let X be compact non empty TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> Banach_Algebra-like; coherence proof set B = R_Normed_Algebra_of_ContinuousFunctions(X); A1:now let f,g be Element of B; reconsider f1=f, g1=g as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; A2: ||.f.|| =||.f1.|| & ||.g.|| =||.g1.|| & ||.f*g.|| =||.f1*g1.|| by Lm6,Lm3; R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_1 by C0SP1:37; hence ||. f*g .|| <= ||.f.|| * ||.g.|| by A2,LOPBAN_2:def 9; end; A3:R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by C0SP1:37; A4:||.(1.B).||=||. 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X.|| by Lm8,Lm3 .= 1 by A3,LOPBAN_2:def 10; A5:now let a be Real, f,g be Element of B; reconsider f1=f, g1=g as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; A6: a*g1=a*g by Lm5; A7: f*g=f1*g1 by Lm6; A8: R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_3 by C0SP1:37; a*(f*g) =a*(f1*g1) by A7,Lm5; then a*(f*g) =f1*(a*g1) by A8,LOPBAN_2:def 11; hence a*(f*g) =f*(a*g) by A6,Lm6; end; now let f,g,h be Element of B; reconsider f1=f, g1=g, h1=h as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1; A9: g+h = g1+h1 by Lm4; A10:g*f = g1*f1 & h*f = h1*f1 by Lm6; A11:R_Normed_Algebra_of_BoundedFunctions the carrier of X is left-distributive by C0SP1:37; thus (g+h)*f =(g1+h1)*f1 by Lm6,A9 .= g1*f1 + h1*f1 by A11,VECTSP_1:def 3 .= g*f + h*f by Lm4,A10; end; then B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left-distributive left_unital complete Normed_Algebra by A1,A4,A5,LOPBAN_2:def 9,def 10,def 11,VECTSP_1:def 3; hence thesis; end; end; begin :: Some properties of support theorem Th23: for X be non empty TopSpace for f,g be RealMap of X holds support(f+g) c= support(f) \/ support(g) proof let X be non empty TopSpace; let f,g be RealMap of X; set CX= the carrier of X; reconsider h=f+g as RealMap of X; A1:dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1; now let x be set; assume A2:x in (CX\ support(f)) /\ (CX\ support(g)); then x in (CX\ support(f)) & x in (CX\ support(g)) by XBOOLE_0:def 4; then x in CX & not x in support(f) & x in CX & not x in support(g) by XBOOLE_0:def 5; then A3: x in CX & f.x =0 & g.x=0 by PRE_POLY:def 7; A4: (f+g).x = 0 + 0 by A3,VALUED_1:1; not x in support(f+g) by A4,PRE_POLY:def 7; hence x in CX\ support(f+g) by A2,XBOOLE_0:def 5; end; then (CX\ support(f)) /\ (CX \ support(g)) c= CX\ support(f+g) by TARSKI:def 3; then CX\ ( support(f) \/ support(g) ) c= CX\ support(f+g) by XBOOLE_1:53; then CX\ (CX\ support(f+g)) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:34; then CX/\ support(f+g) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:48; then CX/\ support(f+g) c= CX/\ (support(f) \/ support(g)) by XBOOLE_1:48; then support(f+g) c= CX/\ (support(f) \/ support(g)) by A1,PRE_POLY:37,XBOOLE_1:28; then support(f+g) c= (CX/\ support(f)) \/ (CX/\ support(g)) by XBOOLE_1:23; then support(f+g) c= support(f) \/ (CX/\ support(g)) by A1,PRE_POLY:37,XBOOLE_1:28; hence thesis by A1,PRE_POLY:37,XBOOLE_1:28; end; theorem Th24: for X be non empty TopSpace for a be Real,f be RealMap of X holds support(a(#)f) c= support(f) proof let X be non empty TopSpace; let a be Real,f be RealMap of X; set CX= the carrier of X; reconsider h=a(#)f as RealMap of X; now let x be set; assume x in support(a(#)f); then (a(#)f).x <>0 by PRE_POLY:def 7; then A1: a*f.x <> 0 by VALUED_1:6; f.x <> 0 by A1; hence x in support(f) by PRE_POLY:def 7; end; hence thesis by TARSKI:def 3; end; theorem for X be non empty TopSpace for f,g be RealMap of X holds support(f(#)g) c= support(f) \/ support(g) proof let X be non empty TopSpace; let f,g be RealMap of X; set CX= the carrier of X; reconsider h=f(#)g as RealMap of X; A1: dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1; now let x be set; assume A2: x in (CX\ support(f)) /\ (CX\ support(g)); then x in (CX\ support(f)) & x in (CX\ support(g)) by XBOOLE_0:def 4; then x in CX& not x in support(f) & x in CX & not x in support(g) by XBOOLE_0:def 5; then A3: x in CX& f.x =0 & g.x=0 by PRE_POLY:def 7; A4: (f(#)g).x = 0 * 0 by A3,VALUED_1:5; not x in support(f(#)g) by A4,PRE_POLY:def 7; hence x in CX\ support(f(#)g) by A2,XBOOLE_0:def 5; end; then (CX\ support(f)) /\ (CX\ support(g)) c= CX\ support(f(#)g) by TARSKI:def 3; then CX\ (support(f) \/ support(g) ) c= CX\ support(f(#)g) by XBOOLE_1:53; then CX\ (CX\ support(f(#)g)) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:34; then CX/\ support(f(#)g) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:48; then CX/\ support(f(#)g) c= CX/\ (support(f) \/ support(g)) by XBOOLE_1:48; then support(f(#)g) c= CX/\ (support(f) \/ support(g)) by A1,PRE_POLY:37,XBOOLE_1:28; then support(f(#)g) c= (CX/\ support(f)) \/ (CX/\ support(g)) by XBOOLE_1:23; then support(f(#)g) c= support(f) \/ (CX/\ support(g)) by A1,PRE_POLY:37,XBOOLE_1:28; hence thesis by A1,PRE_POLY:37,XBOOLE_1:28; end; begin :: Space of Real-valued Continuous Functionals with Bounded Support definition let X be non empty TopSpace; func C_0_Functions(X) -> non empty Subset of RealVectSpace the carrier of X equals { f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))}; correctness proof A1:{ f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))} c= Funcs(the carrier of X,REAL) proof for x being set st x in { f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))} holds x in Funcs(the carrier of X,REAL) proof let x be set; assume x in { f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st( Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))}; then ex f be RealMap of X st x=f & f is continuous & ex Y be non empty Subset of X st ( Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y)); hence x in Funcs(the carrier of X,REAL) by FUNCT_2:8; end; hence thesis by TARSKI:def 3; end; { f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st (Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))} is non empty proof set g= (the carrier of X) --> 0; reconsider g as RealMap of X by FUNCOP_1:46; A2: g is continuous proof for P being Subset of REAL st P is closed holds g"P is closed proof let P being Subset of REAL such that P is closed; set F = (the carrier of X) --> 0, H = the carrier of X; set HX=[#] X; per cases; suppose 0 in P; then g"P = HX by FUNCOP_1:14; hence g"P is closed; end; suppose not 0 in P; then F"P = {}X by FUNCOP_1:16; hence g"P is closed; end; end; hence thesis by PSCOMP_1:def 3; end; A3: ex Y be non empty Subset of X st( Y is compact & (for A being Subset of X st A=support(g) holds Cl(A) is Subset of Y)) proof set S = the compact non empty Subset of X; A4: for A being Subset of X st A=support(g) holds Cl(A) is Subset of S proof let A be Subset of X; assume A5: A=support(g); A6: A={} proof assume A7: not thesis; set p = the Element of support(g); A8: p in A by A7,A5; g.p<>0 by A5,A7,PRE_POLY:def 7; hence contradiction by A8,FUNCOP_1:7; end; Cl(A)={}X by A6,PRE_TOPC:22; hence thesis by XBOOLE_1:2; end; thus thesis by A4; end; g in { f where f is RealMap of X : f is continuous & ex Y be non empty Subset of X st( Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))} by A2,A3; hence thesis; end; hence thesis by A1; end; end; theorem for X be non empty TopSpace holds C_0_Functions(X) is non empty Subset of RAlgebra the carrier of X; Lm10: for X be non empty TopSpace for v,u be Element of RAlgebra the carrier of X st v in C_0_Functions(X) & u in C_0_Functions(X) holds v + u in C_0_Functions(X) proof let X be non empty TopSpace; set W = C_0_Functions(X); set V = RAlgebra the carrier of X; let u,v be Element of V such that A1: u in W & v in W; consider u1 be RealMap of X such that A2: u1=u & u1 is continuous & (ex Y1 be non empty Subset of X st Y1 is compact & (for A1 being Subset of X st A1=support(u1) holds Cl(A1) is Subset of Y1)) by A1; consider Y1 be non empty Subset of X such that A3: (Y1 is compact & (for A1 being Subset of X st A1=support(u1) holds Cl(A1) is Subset of Y1)) by A2; consider v1 be RealMap of X such that A4: v1=v & v1 is continuous & (ex Y2 be non empty Subset of X st Y2 is compact & (for A2 being Subset of X st A2=support(v1) holds Cl(A2) is Subset of Y2)) by A1; consider Y2 be non empty Subset of X such that A5: (Y2 is compact & (for A2 being Subset of X st A2=support(v1) holds Cl(A2) is Subset of Y2)) by A4; A6:u in ContinuousFunctions(X) by A2; A7:v in ContinuousFunctions(X) by A4; v + u in ContinuousFunctions(X) by A6,A7,IDEAL_1:def 1; then consider fvu be continuous RealMap of X such that A8: v+u = fvu; A9:Y1 \/ Y2 is compact by A3,A5,COMPTS_1:10; A10: dom u1 = the carrier of X & dom v1 = the carrier of X by FUNCT_2:def 1; reconsider A1= support(u1),A2= support(v1) as Subset of X by A10,PRE_POLY:37; A11:dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1 .= (the carrier of X) /\ (the carrier of X) by FUNCT_2:def 1 .= (the carrier of X); A12:dom (v1+u1) = dom v1 /\ dom u1 by VALUED_1:def 1; reconsider A1= support(u1),A2= support(v1) as Subset of X by A10,PRE_POLY:37; reconsider A3= support(v1+u1) as Subset of X by A12,A11,PRE_POLY:37; Cl(A3) c= Cl(A2 \/ A1) by Th23,PRE_TOPC:19; then A13:Cl(A3) c= Cl(A2) \/ Cl(A1) by PRE_TOPC:20; A14: Cl(A1) is Subset of Y1 by A3; Cl(A2) is Subset of Y2 by A5; then Cl(A2) \/ Cl(A1) c= Y2 \/ Y1 by A14,XBOOLE_1:13; then A15:for A3 being Subset of X st A3=support(v1+u1) holds Cl(A3) is Subset of Y2 \/ Y1 by A13,XBOOLE_1:1; reconsider vv1=v as Element of Funcs((the carrier of X),REAL); reconsider uu1=u as Element of Funcs((the carrier of X),REAL); reconsider fvu1=v+u as Element of Funcs((the carrier of X),REAL); A16:dom fvu1 = the carrier of X by FUNCT_2:def 1; for c being set st c in dom fvu1 holds fvu1.c = v1.c + u1.c by A2,A4,FUNCSDOM:1; then fvu1 = v1+u1 by A16,A11,VALUED_1:def 1; hence thesis by A8,A9,A15; end; Lm11: for X be non empty TopSpace for a be Real,u be Element of RAlgebra the carrier of X st u in C_0_Functions(X) holds a * u in C_0_Functions(X) proof let X be non empty TopSpace; set W = C_0_Functions(X); set V = RAlgebra the carrier of X; let a be Real; let u be Element of V; assume A1: u in W; consider u1 be RealMap of X such that A2: u1=u & u1 is continuous & (ex Y1 be non empty Subset of X st Y1 is compact & (for A1 being Subset of X st A1=support(u1) holds Cl(A1) is Subset of Y1)) by A1; consider Y1 be non empty Subset of X such that A3: (Y1 is compact & (for A1 being Subset of X st A1=support(u1) holds Cl(A1) is Subset of Y1)) by A2; A4:u in ContinuousFunctions(X) by A2; a * u in ContinuousFunctions(X) by A4,C0SP1:def 10; then consider fau being continuous RealMap of X such that A5: fau = a*u; A6: dom u1 = the carrier of X by FUNCT_2:def 1; then reconsider A1= support(u1) as Subset of X by PRE_POLY:37; A7:dom u1 = (the carrier of X) by FUNCT_2:def 1; A8: dom (a(#)u1) = dom u1 by VALUED_1:def 5; reconsider A1= support(u1) as Subset of X by A6,PRE_POLY:37; reconsider A3= support(a(#)u1) as Subset of X by A8,A7,PRE_POLY:37; A9:Cl(A1) is Subset of Y1 by A3; Cl(A3) c= Cl(A1) by Th24,PRE_TOPC:19; then A10:for A3 being Subset of X st A3=support(a(#)u1) holds Cl(A3) is Subset of Y1 by A9,XBOOLE_1:1; reconsider uu1=u as Element of Funcs((the carrier of X),REAL); reconsider fau1=a*u as Element of Funcs((the carrier of X),REAL); A11:dom fau1 = the carrier of X by FUNCT_2:def 1; A12:dom u1 = the carrier of X by FUNCT_2:def 1; for c being set st c in dom fau1 holds fau1.c = a * u1.c by A2,FUNCSDOM:4; then fau1 = a(#)u1 by A11,A12,VALUED_1:def 5; hence thesis by A3,A10,A5; end; Lm12: for X be non empty TopSpace for u be Element of RAlgebra the carrier of X st u in C_0_Functions(X) holds -u in C_0_Functions(X) proof let X be non empty TopSpace; set W = C_0_Functions(X); set V = RAlgebra the carrier of X; let u be Element of V; assume A1: u in W; set a=-1; RAlgebra the carrier of X is RealLinearSpace by C0SP1:7; then -u = a*u by RLVECT_1:16; hence thesis by Lm11,A1; end; theorem for X be non empty TopSpace for W be non empty Subset of RAlgebra the carrier of X st W = C_0_Functions(X) holds W is additively-linearly-closed proof let X be non empty TopSpace; let W be non empty Subset of RAlgebra the carrier of X; assume A1: W = C_0_Functions(X); set V = RAlgebra the carrier of X; for v,u be Element of V st v in W & u in W holds v + u in W by A1,Lm10; then A2:W is add-closed by IDEAL_1:def 1; for v be Element of V st v in W holds -v in W by A1,Lm12; then A3:W is having-inverse by C0SP1:def 1; for a be Real, u be Element of V st u in W holds a * u in W by A1,Lm11; hence W is additively-linearly-closed by A2,A3,C0SP1:def 10; end; theorem Th28: for X be non empty TopSpace holds C_0_Functions(X) is linearly-closed proof let X be non empty TopSpace; set Y = C_0_Functions(X); set V = RealVectSpace(the carrier of X); A1:for v,u be VECTOR of V st v in Y & u in Y holds v + u in Y proof let v,u be VECTOR of V; assume A2: v in Y & u in Y; reconsider v1=v, u1=u as Element of Funcs((the carrier of X),REAL); reconsider v2=v, u2=u as VECTOR of RAlgebra the carrier of X; v2+u2 in Y by A2,Lm10; hence thesis; end; for a be Real, v be Element of V st v in Y holds a * v in Y proof let a be Real,v be VECTOR of V; assume A3: v in Y; reconsider v1=v as Element of Funcs((the carrier of X),REAL); reconsider v2=v as VECTOR of RAlgebra the carrier of X; a*v2 in Y by A3,Lm11; hence thesis; end; hence thesis by A1,RLSUB_1:def 1; end; registration let X be non empty TopSpace; cluster C_0_Functions(X) -> non empty linearly-closed; correctness by Th28; end; definition let X be non empty TopSpace; func R_VectorSpace_of_C_0_Functions(X) -> RealLinearSpace equals RLSStruct (# C_0_Functions(X), Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)), Add_(C_0_Functions(X), RealVectSpace(the carrier of X)), Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)) #); correctness by RSSPACE:11; end; theorem for X be non empty TopSpace holds R_VectorSpace_of_C_0_Functions(X) is Subspace of RealVectSpace(the carrier of X) by RSSPACE:11; theorem Th30: for X be non empty TopSpace for x being set st x in C_0_Functions(X) holds x in BoundedFunctions the carrier of X proof let X be non empty TopSpace; let x be set such that A1: x in C_0_Functions(X); consider f be RealMap of X such that A2: f=x & f is continuous & (ex Y be non empty Subset of X st Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y)) by A1; consider Y be non empty Subset of X such that A3: (Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y)) by A2; dom f = the carrier of X by FUNCT_2:def 1; then reconsider A= support(f) as Subset of X by PRE_POLY:37; reconsider Y1 = f.:Y as non empty real-bounded Subset of REAL by A2,A3,JORDAN_A:1,RCOMP_1:10; A4:Y1 c= [. inf Y1,sup Y1 .] by XXREAL_2:69; reconsider r1 = inf Y1, r2 = sup Y1 as real number; consider r be real number such that A5: r=abs(r1)+abs(r2)+1; for p being Element of Y holds r>0 & -r< f.p & f.p =0 & abs(r2)>=0 by COMPLEX1:46; -abs(r1) <= r1 by ABSVALUE:4; then -abs(r1) - abs(r2) <= r1 - 0 by A7,XREAL_1:13; then -abs(r1) - abs(r2) - 1 < r1 - 0 by XREAL_1:15; then A8:-r < r1 by A5; r2 <= abs(r2) by ABSVALUE:4; then r2 + 0 <= abs(r2)+abs(r1) by A7,XREAL_1:7; then r2 < r by A5,XREAL_1:8; hence thesis by A6,A8,XXREAL_0:2; end; then consider r be real number such that A9: for p being Element of Y holds r>0 & -r< f.p & f.p Function of (C_0_Functions(X)),REAL equals (BoundedFunctionsNorm the carrier of X)|(C_0_Functions(X)); correctness proof for x being set st x in C_0_Functions(X) holds x in BoundedFunctions the carrier of X by Th30; then C_0_Functions(X) c= BoundedFunctions the carrier of X by TARSKI:def 3; hence thesis by FUNCT_2:32; end; end; definition let X be non empty TopSpace; func R_Normed_Space_of_C_0_Functions(X) -> non empty NORMSTR equals NORMSTR (# C_0_Functions(X), Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)), Add_(C_0_Functions(X), RealVectSpace(the carrier of X)), Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)), C_0_FunctionsNorm X #); correctness; end; registration let X be non empty TopSpace; cluster R_Normed_Space_of_C_0_Functions(X) -> strict non empty; correctness; end; theorem for X be non empty TopSpace for x being set st x in C_0_Functions(X) holds x in ContinuousFunctions(X) proof let X be non empty TopSpace; let x be set such that A1: x in C_0_Functions(X); consider f be RealMap of X such that A2: f=x & f is continuous & (ex Y be non empty Subset of X st Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y)) by A1; thus thesis by A2; end; theorem Th32: for X be non empty TopSpace holds 0.R_VectorSpace_of_C_0_Functions(X) = X -->0 proof let X be non empty TopSpace; A1:R_VectorSpace_of_C_0_Functions(X) is Subspace of RealVectSpace(the carrier of X) by RSSPACE:11; 0.RealVectSpace(the carrier of X) = X -->0; hence thesis by A1,RLSUB_1:11; end; theorem Th33: for X be non empty TopSpace holds 0.R_Normed_Space_of_C_0_Functions(X) = X --> 0 proof let X be non empty TopSpace; 0.R_Normed_Space_of_C_0_Functions(X) =0.R_VectorSpace_of_C_0_Functions(X) .=X --> 0 by Th32; hence thesis; end; Lm13: for X be non empty TopSpace for x1,x2 be Point of R_Normed_Space_of_C_0_Functions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x1=y1 & x2=y2 holds x1+x2=y1+y2 proof let X be non empty TopSpace; let x1,x2 be Point of R_Normed_Space_of_C_0_Functions(X), y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x1=y1 & x2=y2; thus x1+x2 = ((the addF of RealVectSpace(the carrier of X)) ||C_0_Functions(X)).([x1,x2]) by RSSPACE:def 8 .= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49 .= ((the addF of RAlgebra the carrier of X) ||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49 .=y1+y2 by C0SP1:def 5; end; Lm14: for X be non empty TopSpace for a be Real,x be Point of R_Normed_Space_of_C_0_Functions(X), y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X st x=y holds a*x=a*y proof let X be non empty TopSpace; let a be Real, x be Point of R_Normed_Space_of_C_0_Functions(X), y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; assume A1: x=y; thus a*x = ((the Mult of RAlgebra the carrier of X)| [:REAL,(C_0_Functions(X)):]).([a,x]) by RSSPACE:def 9 .= (the Mult of RAlgebra the carrier of X).([a,x]) by FUNCT_1:49 .= ((the Mult of RAlgebra the carrier of X) |[:REAL,(BoundedFunctions the carrier of X):]).([a,y]) by A1,FUNCT_1:49 .=a*y by C0SP1:def 11; end; theorem Th34: for a be Real for X be non empty TopSpace for F,G be Point of R_Normed_Space_of_C_0_Functions(X) holds (||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions(X) ) & ||.a*F.|| = abs a * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.|| proof let a be Real; let X be non empty TopSpace; let F,G be Point of R_Normed_Space_of_C_0_Functions(X); A1:||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions(X) proof reconsider FB=F as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30; A2: 0.R_Normed_Space_of_C_0_Functions(X) =X-->0 by Th33; ||.FB.|| = 0 iff FB = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:32; hence thesis by A2,C0SP1:25,FUNCT_1:49; end; A3:||.a*F.|| = abs a * ||.F.|| proof reconsider FB=F as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30; A4: ||.FB.||=||.F.|| by FUNCT_1:49; A5: a*FB=a*F by Lm14; reconsider aFB=a*FB as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; reconsider aF=a*F as Point of R_Normed_Space_of_C_0_Functions(X); ||.aFB.||=||.aF.|| by A5,FUNCT_1:49; hence thesis by A4,C0SP1:32; end; ||.F+G.|| <= ||.F.|| + ||.G.|| proof reconsider FB=F,GB=G as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30; A6:||.FB.||=||.F.|| & ||.GB.||=||.G.|| by FUNCT_1:49; FB+GB=F+G by Lm13; then A7:||.FB+GB.||=||.F+G.|| by FUNCT_1:49; reconsider aFB=FB+GB as Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X; reconsider aF=F,aG=G as Point of R_Normed_Space_of_C_0_Functions(X); thus thesis by A7,A6,C0SP1:32; end; hence thesis by A1,A3; end; theorem Th35: for X be non empty TopSpace holds R_Normed_Space_of_C_0_Functions(X) is RealNormSpace-like proof let X be non empty TopSpace; for x, y being Point of R_Normed_Space_of_C_0_Functions(X) for a be Real holds ||.a*x.|| = abs(a) * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th34; hence thesis by NORMSP_1:def 1; end; registration let X be non empty TopSpace; cluster R_Normed_Space_of_C_0_Functions(X) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence proof A1:R_VectorSpace_of_C_0_Functions(X) is RealLinearSpace; A2:for x be Point of R_Normed_Space_of_C_0_Functions(X) st ||.x.|| = 0 holds x = 0.(R_Normed_Space_of_C_0_Functions(X)) by Th34; ||.0.(R_Normed_Space_of_C_0_Functions(X)).|| = 0 by Th34; hence thesis by A1,A2,Th35,NORMSP_0:def 5,def 6,RSSPACE3:2; end; end; theorem for X be non empty TopSpace holds R_Normed_Space_of_C_0_Functions(X) is RealNormSpace;