begin
Lm1:
for V being non empty addLoopStr holds [#] V is add-closed
Lm2:
for V being non empty addLoopStr holds [#] V is having-inverse
begin
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
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 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
begin
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) #);
Lm4:
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;