environ
vocabularies HIDDEN, STRUCT_0, 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, FUNCT_7;
notations HIDDEN, 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;
definitions PSCOMP_1, TARSKI, FUNCSDOM, RLVECT_1, VECTSP_1, GROUP_1, 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, PRE_POLY, XBOOLE_0, RSSPACE, COMPTS_1, PRE_TOPC, RLSUB_1, JORDAN_A, NAGATA_1, JGRAPH_2, TOPMETR, JORDAN5A, XXREAL_2, ORDINAL1;
schemes ;
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;
constructors HIDDEN, REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, C0SP1, NFCONT_1, SEQFUNC, MEASURE6, PRE_POLY, TOPMETR, RLSUB_1, SEQ_4, NAGATA_1, PSCOMP_1, COMPTS_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities REALSET1, ALGSTR_0, XCMPLX_0, RCOMP_1, FUNCSDOM, RLVECT_1, STRUCT_0, BINOP_1, C0SP1, NORMSP_0;
expansions PSCOMP_1, ALGSTR_0, TARSKI, RCOMP_1, RLVECT_1, C0SP1, NORMSP_0;
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
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))) #) is AlgebraStr
;
end;
::
deftheorem defines
R_Algebra_of_ContinuousFunctions C0SP2:def 3 :
for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X = 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))) #);
Lm1:
for X being non empty compact TopSpace
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
definition
let X be non
empty compact 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
coherence
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) #) is Normed_AlgebraStr ;
;
end;
::
deftheorem defines
R_Normed_Algebra_of_ContinuousFunctions C0SP2:def 5 :
for X being non empty compact TopSpace holds R_Normed_Algebra_of_ContinuousFunctions X = 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) #);
Lm2:
now for X being non empty compact TopSpace
for x, e being Element of (R_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) holds
( x * e = x & e * x = x )
let X be non
empty compact TopSpace;
for x, e being Element of (R_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) holds
( x * e = x & e * x = x )set F =
R_Normed_Algebra_of_ContinuousFunctions X;
let x,
e be
Element of
(R_Normed_Algebra_of_ContinuousFunctions X);
( e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )assume A1:
e = One_ (
(ContinuousFunctions X),
(RAlgebra the carrier of X))
;
( x * e = x & e * x = x )set X1 =
ContinuousFunctions X;
reconsider f =
x as
Element of
ContinuousFunctions X ;
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 [:(ContinuousFunctions X),(ContinuousFunctions X):] &
[(1_ (RAlgebra the carrier of X)),f] in [:(ContinuousFunctions X),(ContinuousFunctions X):] )
by ZFMISC_1:87;
x * e = (mult_ ((ContinuousFunctions X),(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) || (ContinuousFunctions X)) . (
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 = x
e * x = (mult_ ((ContinuousFunctions X),(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) || (ContinuousFunctions X)) . (
(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;
verum
end;
Lm3:
for X being non empty compact TopSpace
for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being 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 non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
Lm5:
for X being non empty compact TopSpace
for a being Real
for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
Lm6:
for X being non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm7:
for X being non empty compact TopSpace holds 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
Lm8:
for X being non empty compact TopSpace holds 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
Lm9:
for X being non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
Lm10:
for X being non empty TopSpace
for v, u being 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
Lm11:
for X being non empty TopSpace
for a being Real
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
Lm12:
for X being non empty TopSpace
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
- u in C_0_Functions X
Lm13:
for X being non empty TopSpace
for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
Lm14:
for X being non empty TopSpace
for a being Real
for x being Point of (R_Normed_Space_of_C_0_Functions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y