environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3, FUNCSDOM, STRUCT_0, TARSKI, REALSET1, MESFUNC1, SUPINF_2, BINOP_1, FUNCT_1, ZFMISC_1, RELAT_1, RLVECT_1, VECTSP_1, LATTICES, RSSPACE, GROUP_1, REAL_1, POLYALG1, CARD_1, RSSPACE4, XXREAL_2, FUNCOP_1, FUNCT_2, VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, SEQ_4, ORDINAL2, LOPBAN_2, PRE_TOPC, NORMSP_1, NAT_1, RSSPACE3, SEQ_2, SEQ_1, REWRITE1, C0SP1, METRIC_1, RELAT_2, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, STRUCT_0, ALGSTR_0, REAL_1, REALSET1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, RELSET_1, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, PARTFUN1, IDEAL_1, RSSPACE3, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCOP_1, NORMSP_0, NORMSP_1, LOPBAN_1, LOPBAN_2;
definitions ALGSTR_0, TARSKI, FUNCSDOM, RLVECT_1, VECTSP_1, GROUP_1, NORMSP_0, XXREAL_2, LOPBAN_2;
theorems SEQ_4, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, ALGSTR_0, COMPLEX1, ZFMISC_1, TARSKI, RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, GROUP_1, VALUED_1, RSSPACE2, IDEAL_1, RELSET_1, NORMSP_0, ORDINAL1;
schemes SEQ_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, XXREAL_0, RLVECT_1, VECTSP_1, VECTSP_2, FUNCT_2, VALUED_0, VALUED_1, LOPBAN_2, FUNCOP_1, SEQ_4, RFUNCT_1, RELSET_1, SEQ_1, SEQ_2;
constructors HIDDEN, REAL_1, REALSET1, RSSPACE3, COMPLEX1, BINOP_2, LOPBAN_2, SEQ_2, IDEAL_1, SEQ_4, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities REALSET1, ALGSTR_0, XCMPLX_0, FUNCSDOM, RLVECT_1, STRUCT_0, BINOP_1, VALUED_1, NORMSP_0;
expansions ALGSTR_0, NORMSP_0, LOPBAN_2;
Lm1:
for V being non empty addLoopStr holds [#] V is add-closed
theorem Th3:
for
X being non
empty set for
d1,
d2 being
Element of
X for
A being
BinOp of
X for
M being
Function of
[:X,X:],
X for
V being
Algebra for
V1 being
Subset of
V for
MR being
Function of
[:REAL,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 | [:REAL,V1:] &
V1 is
having-inverse holds
AlgebraStr(#
X,
M,
A,
MR,
d2,
d1 #) is
Subalgebra of
V
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace
by RLVECT_1:def 8;
theorem Th6:
for
V being
Algebra for
V1 being
Subset of
V st
V1 is
additively-linearly-closed &
V1 is
multiplicatively-closed & not
V1 is
empty holds
AlgebraStr(#
V1,
(mult_ (V1,V)),
(Add_ (V1,V)),
(Mult_ (V1,V)),
(One_ (V1,V)),
(Zero_ (V1,V)) #) is
Subalgebra of
V
definition
let X be non
empty set ;
func R_Algebra_of_BoundedFunctions X -> Algebra equals
AlgebraStr(#
(BoundedFunctions X),
(mult_ ((BoundedFunctions X),(RAlgebra X))),
(Add_ ((BoundedFunctions X),(RAlgebra X))),
(Mult_ ((BoundedFunctions X),(RAlgebra X))),
(One_ ((BoundedFunctions X),(RAlgebra X))),
(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);
coherence
AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #) is Algebra
by Th6;
end;
::
deftheorem defines
R_Algebra_of_BoundedFunctions C0SP1:def 14 :
for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))) #);
definition
let X be non
empty set ;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals
Normed_AlgebraStr(#
(BoundedFunctions X),
(mult_ ((BoundedFunctions X),(RAlgebra X))),
(Add_ ((BoundedFunctions X),(RAlgebra X))),
(Mult_ ((BoundedFunctions X),(RAlgebra X))),
(One_ ((BoundedFunctions X),(RAlgebra X))),
(Zero_ ((BoundedFunctions X),(RAlgebra X))),
(BoundedFunctionsNorm X) #);
correctness
coherence
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;
;
end;
::
deftheorem defines
R_Normed_Algebra_of_BoundedFunctions C0SP1:def 18 :
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ ((BoundedFunctions X),(RAlgebra X))),(Add_ ((BoundedFunctions X),(RAlgebra X))),(Mult_ ((BoundedFunctions X),(RAlgebra X))),(One_ ((BoundedFunctions X),(RAlgebra X))),(Zero_ ((BoundedFunctions X),(RAlgebra X))),(BoundedFunctionsNorm X) #);
Lm3:
now for X being non empty set
for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds
( x * e = x & e * x = x )
let X be non
empty set ;
for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((BoundedFunctions X),(RAlgebra X)) holds
( x * e = x & e * x = x )set F =
R_Normed_Algebra_of_BoundedFunctions X;
let x,
e be
Element of
(R_Normed_Algebra_of_BoundedFunctions X);
( e = One_ ((BoundedFunctions X),(RAlgebra X)) implies ( x * e = x & e * x = x ) )set X1 =
BoundedFunctions X;
reconsider f =
x as
Element of
BoundedFunctions X ;
assume A1:
e = One_ (
(BoundedFunctions X),
(RAlgebra X))
;
( x * e = x & e * x = x )then
x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (
f,
(1_ (RAlgebra X)))
by Def8;
then A2:
x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (
f,
(1_ (RAlgebra X)))
by Def6;
e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (
(1_ (RAlgebra X)),
f)
by A1, Def8;
then A3:
e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (
(1_ (RAlgebra X)),
f)
by Def6;
A4:
1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X)
by Th16;
then
[f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):]
by ZFMISC_1:87;
then
x * e = f * (1_ (RAlgebra X))
by A2, FUNCT_1:49;
hence
x * e = x
by VECTSP_1:def 4;
e * x = x
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):]
by A4, ZFMISC_1:87;
then
e * x = (1_ (RAlgebra X)) * f
by A3, FUNCT_1:49;
hence
e * x = x
by VECTSP_1:def 4;
verum
end;