begin
:: deftheorem Def1 defines having-inverse C0SP1:def 1 :
:: deftheorem Def2 defines additively-closed C0SP1:def 2 :
Lm1:
for V being non empty addLoopStr holds [#] V is add-closed
Lm2:
for V being non empty addLoopStr holds [#] V is having-inverse
:: deftheorem Def3 defines Subring C0SP1:def 3 :
theorem Th1:
:: deftheorem Def4 defines multiplicatively-closed C0SP1:def 4 :
:: deftheorem Def5 defines Add_ C0SP1:def 5 :
:: deftheorem Def6 defines mult_ C0SP1:def 6 :
:: deftheorem Def7 defines Zero_ C0SP1:def 7 :
:: deftheorem Def8 defines One_ C0SP1:def 8 :
theorem
begin
:: deftheorem Def9 defines Subalgebra C0SP1:def 9 :
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
:: deftheorem Def10 defines additively-linearly-closed C0SP1:def 10 :
:: deftheorem Def11 defines Mult_ C0SP1:def 11 :
:: deftheorem Def12 defines scalar-mult-cancelable C0SP1:def 12 :
theorem Th4:
theorem
Lm3:
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 11;
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
theorem Th7:
theorem Th8:
begin
:: deftheorem defines BoundedFunctions C0SP1:def 13 :
theorem Th9:
theorem
for
X being non
empty set holds
AlgebraStr(#
(BoundedFunctions X),
(mult_ (BoundedFunctions X),(RAlgebra X)),
(Add_ (BoundedFunctions X),(RAlgebra X)),
(Mult_ (BoundedFunctions X),(RAlgebra X)),
(One_ (BoundedFunctions X),(RAlgebra X)),
(Zero_ (BoundedFunctions X),(RAlgebra X)) #) is
Subalgebra of
RAlgebra X by Th6;
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)) #);
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem Def15 defines modetrans C0SP1:def 15 :
:: deftheorem defines PreNorms C0SP1:def 16 :
theorem Th17:
theorem
theorem Th19:
:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def 17 :
theorem Th20:
theorem Th21:
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) #);
Lm4:
now
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:106;
then
x * e = f * (1_ (RAlgebra X))
by A2, FUNCT_1:72;
hence
x * e = x
by VECTSP_1:def 13;
e * x = x
[(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):]
by A4, ZFMISC_1:106;
then
e * x = (1_ (RAlgebra X)) * f
by A3, FUNCT_1:72;
hence
e * x = x
by VECTSP_1:def 13;
verum
end;
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem