environ
vocabularies HIDDEN, STRUCT_0, FUNCOP_1, NUMBERS, PRE_TOPC, ORDINAL2, SUBSET_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, COMPLEX1, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, BINOP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, XXREAL_2, XXREAL_0, NORMSP_1, REWRITE1, NAT_1, RSSPACE3, SEQ_2, PARTFUN1, SEQ_1, LOPBAN_1, SEQ_4, CFUNCDOM, CLVECT_1, VECTSP_1, RELAT_2, CC0SP1, XCMPLX_0, CLOPBAN2, LOPBAN_2, METRIC_1, COMSEQ_1, CSSPACE4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, REALSET1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, IDEAL_1, CLVECT_1, CFUNCDOM, CLOPBAN2, C0SP1, CLOPBAN1, COMSEQ_1, CSSPACE3, COMSEQ_2;
definitions ALGSTR_0, TARSKI, RLVECT_1, VECTSP_1, GROUP_1, C0SP1, CFUNCDOM, CLVECT_1, NORMSP_0;
theorems RFUNCT_1, FUNCT_1, SEQ_2, ALGSTR_0, COMPLEX1, ZFMISC_1, TARSKI, IDEAL_1, RELAT_1, XREAL_0, XXREAL_0, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, GROUP_1, VALUED_1, C0SP1, SEQ_4, XXREAL_2, CFUNCDOM, CLVECT_1, RELSET_1, RSSPACE2, CFUNCT_1, CLOPBAN2, NORMSP_0, CSSPACE3, COMSEQ_3, COMSEQ_2, CFCONT_1, CLOPBAN1, ORDINAL1;
schemes SEQ_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, VECTSP_1, VECTSP_2, VALUED_0, C0SP1, XXREAL_0, FUNCT_2, VALUED_1, RFUNCT_1, COMPLEX1, FUNCOP_1, CFUNCDOM, CLVECT_1, XCMPLX_0, COMSEQ_2, CLOPBAN2, RELSET_1, SEQ_2;
constructors HIDDEN, REAL_1, REALSET1, COMPLEX1, IDEAL_1, C0SP1, PARTFUN3, BINOP_2, TOPMETR, SEQ_4, MEASURE6, CLOPBAN2, CSSPACE3, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities REALSET1, ALGSTR_0, XCMPLX_0, STRUCT_0, BINOP_1, VALUED_1, CFUNCDOM, CLVECT_1, COMPLEX1, NORMSP_0;
expansions ALGSTR_0, VECTSP_1, C0SP1, CLVECT_1, NORMSP_0;
Lm1:
now for z being Complex
for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let z be
Complex;
for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet X be non
empty set ;
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet V be
ComplexAlgebra;
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet V1 be non
empty Subset of
V;
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet d1,
d2 be
Element of
X;
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet A be
BinOp of
X;
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet M be
Function of
[:X,X:],
X;
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet MR be
Function of
[:COMPLEX,X:],
X;
( V1 = X & MR = the Mult of V | [:COMPLEX,V1:] implies for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )assume that A1:
V1 = X
and A2:
MR = the
Mult of
V | [:COMPLEX,V1:]
;
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet W be non
empty ComplexAlgebraStr ;
( W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) implies for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )assume A3:
W = ComplexAlgebraStr(#
X,
M,
A,
MR,
d2,
d1 #)
;
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * vlet w be
VECTOR of
W;
for v being Element of V st w = v holds
z * w = z * vlet v be
Element of
V;
( w = v implies z * w = z * v )assume A4:
w = v
;
z * w = z * v
z in COMPLEX
by XCMPLX_0:def 2;
then
[z,w] in [:COMPLEX,V1:]
by A1, A3, ZFMISC_1:def 2;
hence
z * w = z * v
by A4, A2, A3, FUNCT_1:49;
verum
end;
theorem Th1:
for
X being non
empty set for
V being
ComplexAlgebra for
V1 being non
empty Subset of
V for
d1,
d2 being
Element of
X for
A being
BinOp of
X for
M being
Function of
[:X,X:],
X for
MR being
Function of
[:COMPLEX,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 | [:COMPLEX,V1:] &
V1 is
having-inverse holds
ComplexAlgebraStr(#
X,
M,
A,
MR,
d2,
d1 #) is
ComplexSubAlgebra of
V
theorem Th2:
for
V being
ComplexAlgebra for
V1 being non
empty multiplicatively-closed Cadditively-linearly-closed Subset of
V holds
ComplexAlgebraStr(#
V1,
(mult_ (V1,V)),
(Add_ (V1,V)),
(Mult_ (V1,V)),
(One_ (V1,V)),
(Zero_ (V1,V)) #) is
ComplexSubAlgebra of
V
definition
let X be non
empty set ;
func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals
ComplexAlgebraStr(#
(ComplexBoundedFunctions X),
(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
coherence
ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #) is ComplexAlgebra
by Th2;
end;
::
deftheorem defines
C_Algebra_of_BoundedFunctions CC0SP1:def 6 :
for X being non empty set holds C_Algebra_of_BoundedFunctions X = ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
Lm2:
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
definition
let X be non
empty set ;
func C_Normed_Algebra_of_BoundedFunctions X -> Normed_Complex_AlgebraStr equals
Normed_Complex_AlgebraStr(#
(ComplexBoundedFunctions X),
(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),
(ComplexBoundedFunctionsNorm X) #);
correctness
coherence
Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #) is Normed_Complex_AlgebraStr ;
;
end;
::
deftheorem defines
C_Normed_Algebra_of_BoundedFunctions CC0SP1:def 10 :
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X = Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);
Lm3:
now for X being non empty set
for x, e being Element of (C_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) holds
( x * e = x & e * x = x )
let X be non
empty set ;
for x, e being Element of (C_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) holds
( x * e = x & e * x = x )set F =
C_Normed_Algebra_of_BoundedFunctions X;
let x,
e be
Element of
(C_Normed_Algebra_of_BoundedFunctions X);
( e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) implies ( x * e = x & e * x = x ) )set X1 =
ComplexBoundedFunctions X;
reconsider f =
x as
Element of
ComplexBoundedFunctions X ;
assume A1:
e = One_ (
(ComplexBoundedFunctions X),
(CAlgebra X))
;
( x * e = x & e * x = x )then
x * e = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (
f,
(1_ (CAlgebra X)))
by C0SP1:def 8;
then A2:
x * e = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . (
f,
(1_ (CAlgebra X)))
by C0SP1:def 6;
e * x = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (
(1_ (CAlgebra X)),
f)
by A1, C0SP1:def 8;
then A3:
e * x = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . (
(1_ (CAlgebra X)),
f)
by C0SP1:def 6;
A4:
1_ (CAlgebra X) = 1_ (C_Algebra_of_BoundedFunctions X)
by Th9;
then
[f,(1_ (CAlgebra X))] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):]
by ZFMISC_1:87;
then
x * e = f * (1_ (CAlgebra X))
by A2, FUNCT_1:49;
hence
x * e = x
by VECTSP_1:def 4;
e * x = x
[(1_ (CAlgebra X)),f] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):]
by A4, ZFMISC_1:87;
then
e * x = (1_ (CAlgebra X)) * f
by A3, FUNCT_1:49;
hence
e * x = x
by VECTSP_1:def 4;
verum
end;
Lm4:
for X being non empty set holds
( C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
by Th25;