:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received November 20, 2010

:: Copyright (c) 2010-2017 Association of Mizar Users

definition

let V be ComplexAlgebra;

ex b_{1} being ComplexAlgebra st

( the carrier of b_{1} c= the carrier of V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the multF of b_{1} = the multF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:COMPLEX, the carrier of b_{1}:] & 1. b_{1} = 1. V & 0. b_{1} = 0. V )

end;
mode ComplexSubAlgebra of V -> ComplexAlgebra means :Def1: :: CC0SP1:def 1

( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );

existence ( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );

ex b

( the carrier of b

proof end;

:: deftheorem Def1 defines ComplexSubAlgebra CC0SP1:def 1 :

for V, b_{2} being ComplexAlgebra holds

( b_{2} is ComplexSubAlgebra of V iff ( the carrier of b_{2} c= the carrier of V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the multF of b_{2} = the multF of V || the carrier of b_{2} & the Mult of b_{2} = the Mult of V | [:COMPLEX, the carrier of b_{2}:] & 1. b_{2} = 1. V & 0. b_{2} = 0. V ) );

for V, b

( b

Lm1: now :: thesis: 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

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; :: thesis: 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 X be non empty set ; :: thesis: 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 V be ComplexAlgebra; :: thesis: 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 V1 be non empty Subset of V; :: thesis: 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 d1, d2 be Element of X; :: thesis: 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 A be BinOp of X; :: thesis: 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 M be Function of [:X,X:],X; :: thesis: 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 MR be Function of [:COMPLEX,X:],X; :: thesis: ( 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:] ; :: thesis: 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 W be non empty ComplexAlgebraStr ; :: thesis: ( 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 #) ; :: thesis: for w being VECTOR of W

for v being Element of V st w = v holds

z * w = z * v

let w be VECTOR of W; :: thesis: for v being Element of V st w = v holds

z * w = z * v

let v be Element of V; :: thesis: ( w = v implies z * w = z * v )

assume A4: w = v ; :: thesis: 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; :: thesis: verum

end;
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 X be non empty set ; :: thesis: 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 V be ComplexAlgebra; :: thesis: 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 V1 be non empty Subset of V; :: thesis: 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 d1, d2 be Element of X; :: thesis: 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 A be BinOp of X; :: thesis: 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 M be Function of [:X,X:],X; :: thesis: 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 MR be Function of [:COMPLEX,X:],X; :: thesis: ( 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:] ; :: thesis: 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 W be non empty ComplexAlgebraStr ; :: thesis: ( 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 #) ; :: thesis: for w being VECTOR of W

for v being Element of V st w = v holds

z * w = z * v

let w be VECTOR of W; :: thesis: for v being Element of V st w = v holds

z * w = z * v

let v be Element of V; :: thesis: ( w = v implies z * w = z * v )

assume A4: w = v ; :: thesis: 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; :: thesis: verum

theorem Th1: :: CC0SP1:1

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

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

proof end;

registration

let V be ComplexAlgebra;

ex b_{1} being ComplexSubAlgebra of V st b_{1} is strict

end;
cluster non empty right_complementable Abelian add-associative right_zeroed right-distributive right_unital well-unital left_unital unital associative commutative vector-distributive scalar-distributive scalar-associative strict vector-associative for ComplexSubAlgebra of V;

existence ex b

proof end;

definition

let V be ComplexAlgebra;

let V1 be Subset of V;

end;
let V1 be Subset of V;

attr V1 is Cadditively-linearly-closed means :Def2: :: CC0SP1:def 2

( V1 is add-closed & V1 is having-inverse & ( for a being Complex

for v being Element of V st v in V1 holds

a * v in V1 ) );

( V1 is add-closed & V1 is having-inverse & ( for a being Complex

for v being Element of V st v in V1 holds

a * v in V1 ) );

:: deftheorem Def2 defines Cadditively-linearly-closed CC0SP1:def 2 :

for V being ComplexAlgebra

for V1 being Subset of V holds

( V1 is Cadditively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Complex

for v being Element of V st v in V1 holds

a * v in V1 ) ) );

for V being ComplexAlgebra

for V1 being Subset of V holds

( V1 is Cadditively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Complex

for v being Element of V st v in V1 holds

a * v in V1 ) ) );

definition

let V be ComplexAlgebra;

let V1 be Subset of V;

assume A1: ( V1 is Cadditively-linearly-closed & not V1 is empty ) ;

coherence

the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1;

end;
let V1 be Subset of V;

assume A1: ( V1 is Cadditively-linearly-closed & not V1 is empty ) ;

func Mult_ (V1,V) -> Function of [:COMPLEX,V1:],V1 equals :Def3: :: CC0SP1:def 3

the Mult of V | [:COMPLEX,V1:];

correctness the Mult of V | [:COMPLEX,V1:];

coherence

the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1;

proof end;

:: deftheorem Def3 defines Mult_ CC0SP1:def 3 :

for V being ComplexAlgebra

for V1 being Subset of V st V1 is Cadditively-linearly-closed & not V1 is empty holds

Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:];

for V being ComplexAlgebra

for V1 being Subset of V st V1 is Cadditively-linearly-closed & not V1 is empty holds

Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:];

definition

let X be non empty set ;

coherence

{ f where f is Function of X,COMPLEX : f | X is bounded } is non empty Subset of (CAlgebra X);

end;
func ComplexBoundedFunctions X -> non empty Subset of (CAlgebra X) equals :: CC0SP1:def 4

{ f where f is Function of X,COMPLEX : f | X is bounded } ;

correctness { f where f is Function of X,COMPLEX : f | X is bounded } ;

coherence

{ f where f is Function of X,COMPLEX : f | X is bounded } is non empty Subset of (CAlgebra X);

proof end;

:: deftheorem defines ComplexBoundedFunctions CC0SP1:def 4 :

for X being non empty set holds ComplexBoundedFunctions X = { f where f is Function of X,COMPLEX : f | X is bounded } ;

for X being non empty set holds ComplexBoundedFunctions X = { f where f is Function of X,COMPLEX : f | X is bounded } ;

registration

let X be non empty set ;

( ComplexBoundedFunctions X is Cadditively-linearly-closed & ComplexBoundedFunctions X is multiplicatively-closed )

end;
cluster ComplexBoundedFunctions X -> non empty multiplicatively-closed Cadditively-linearly-closed ;

coherence ( ComplexBoundedFunctions X is Cadditively-linearly-closed & ComplexBoundedFunctions X is multiplicatively-closed )

proof end;

registration

let V be ComplexAlgebra;

ex b_{1} being non empty Subset of V st

( b_{1} is Cadditively-linearly-closed & b_{1} is multiplicatively-closed )

end;
cluster non empty multiplicatively-closed Cadditively-linearly-closed for Element of bool the carrier of V;

existence ex b

( b

proof end;

:: deftheorem defines scalar-mult-cancelable CC0SP1:def 5 :

for V being non empty CLSStruct holds

( V is scalar-mult-cancelable iff for a being Complex

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V ) );

for V being non empty CLSStruct holds

( V is scalar-mult-cancelable iff for a being Complex

for v being Element of V holds

( not a * v = 0. V or a = 0 or v = 0. V ) );

theorem Th2: :: CC0SP1:2

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

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

proof end;

theorem Th3: :: CC0SP1:3

for V being ComplexAlgebra

for V1 being ComplexSubAlgebra of V holds

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

for V1 being ComplexSubAlgebra of V holds

( ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 + w1 = v + w ) & ( for v1, w1 being Element of V1

for v, w being Element of V st v1 = v & w1 = w holds

v1 * w1 = v * w ) & ( for v1 being Element of V1

for v being Element of V

for a being Complex st v1 = v holds

a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

definition

let X be non empty set ;

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;
func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals :: CC0SP1:def 6

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))) #);

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;

:: 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))) #);

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))) #);

theorem :: CC0SP1:4

for X being non empty set holds C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;

registration

let X be non empty set ;

coherence

( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital )

end;
coherence

( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital )

proof end;

theorem Th5: :: CC0SP1:5

for X being non empty set

for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th6: :: CC0SP1:6

for X being non empty set

for a being Complex

for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g being Function of X,COMPLEX st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for a being Complex

for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g being Function of X,COMPLEX st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th7: :: CC0SP1:7

for X being non empty set

for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)

for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

definition

let X be non empty set ;

let F be object ;

assume A1: F in ComplexBoundedFunctions X ;

existence

ex b_{1} being Function of X,COMPLEX st

( b_{1} = F & b_{1} | X is bounded );

uniqueness

for b_{1}, b_{2} being Function of X,COMPLEX st b_{1} = F & b_{1} | X is bounded & b_{2} = F & b_{2} | X is bounded holds

b_{1} = b_{2};

by A1;

end;
let F be object ;

assume A1: F in ComplexBoundedFunctions X ;

func modetrans (F,X) -> Function of X,COMPLEX means :Def7: :: CC0SP1:def 7

( it = F & it | X is bounded );

correctness ( it = F & it | X is bounded );

existence

ex b

( b

uniqueness

for b

b

by A1;

:: deftheorem Def7 defines modetrans CC0SP1:def 7 :

for X being non empty set

for F being object st F in ComplexBoundedFunctions X holds

for b_{3} being Function of X,COMPLEX holds

( b_{3} = modetrans (F,X) iff ( b_{3} = F & b_{3} | X is bounded ) );

for X being non empty set

for F being object st F in ComplexBoundedFunctions X holds

for b

( b

definition

let X be non empty set ;

let f be Function of X,COMPLEX;

{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL

end;
let f be Function of X,COMPLEX;

func PreNorms f -> non empty Subset of REAL equals :: CC0SP1:def 8

{ |.(f . x).| where x is Element of X : verum } ;

coherence { |.(f . x).| where x is Element of X : verum } ;

{ |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL

proof end;

:: deftheorem defines PreNorms CC0SP1:def 8 :

for X being non empty set

for f being Function of X,COMPLEX holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;

for X being non empty set

for f being Function of X,COMPLEX holds PreNorms f = { |.(f . x).| where x is Element of X : verum } ;

Lm2: for C being non empty set

for f being PartFunc of C,COMPLEX holds

( |.f.| is bounded iff f is bounded )

proof end;

theorem Th10: :: CC0SP1:10

for X being non empty set

for f being Function of X,COMPLEX st f | X is bounded holds

PreNorms f is bounded_above

for f being Function of X,COMPLEX st f | X is bounded holds

PreNorms f is bounded_above

proof end;

theorem Th11: :: CC0SP1:11

for X being non empty set

for f being Function of X,COMPLEX holds

( f | X is bounded iff PreNorms f is bounded_above )

for f being Function of X,COMPLEX holds

( f | X is bounded iff PreNorms f is bounded_above )

proof end;

definition

let X be non empty set ;

ex b_{1} being Function of (ComplexBoundedFunctions X),REAL st

for x being object st x in ComplexBoundedFunctions X holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X)))

for b_{1}, b_{2} being Function of (ComplexBoundedFunctions X),REAL st ( for x being object st x in ComplexBoundedFunctions X holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being object st x in ComplexBoundedFunctions X holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X))) ) holds

b_{1} = b_{2}

end;
func ComplexBoundedFunctionsNorm X -> Function of (ComplexBoundedFunctions X),REAL means :Def9: :: CC0SP1:def 9

for x being object st x in ComplexBoundedFunctions X holds

it . x = upper_bound (PreNorms (modetrans (x,X)));

existence for x being object st x in ComplexBoundedFunctions X holds

it . x = upper_bound (PreNorms (modetrans (x,X)));

ex b

for x being object st x in ComplexBoundedFunctions X holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CC0SP1:def 9 :

for X being non empty set

for b_{2} being Function of (ComplexBoundedFunctions X),REAL holds

( b_{2} = ComplexBoundedFunctionsNorm X iff for x being object st x in ComplexBoundedFunctions X holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X))) );

for X being non empty set

for b

( b

b

theorem Th12: :: CC0SP1:12

for X being non empty set

for f being Function of X,COMPLEX st f | X is bounded holds

modetrans (f,X) = f

for f being Function of X,COMPLEX st f | X is bounded holds

modetrans (f,X) = f

proof end;

theorem Th13: :: CC0SP1:13

for X being non empty set

for f being Function of X,COMPLEX st f | X is bounded holds

(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

for f being Function of X,COMPLEX st f | X is bounded holds

(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be non empty set ;

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;
func C_Normed_Algebra_of_BoundedFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP1:def 10

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 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) #);

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 ;

;

:: 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) #);

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) #);

registration

let X be non empty set ;

correctness

coherence

not C_Normed_Algebra_of_BoundedFunctions X is empty ;

;

end;
correctness

coherence

not C_Normed_Algebra_of_BoundedFunctions X is empty ;

;

Lm3: now :: thesis: 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 )

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 ; :: thesis: 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); :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

end;
( 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); :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

registration

let X be non empty set ;

correctness

coherence

C_Normed_Algebra_of_BoundedFunctions X is unital ;

end;
correctness

coherence

C_Normed_Algebra_of_BoundedFunctions X is unital ;

proof end;

theorem Th14: :: CC0SP1:14

for W being Normed_Complex_AlgebraStr

for V being ComplexAlgebra st ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds

W is ComplexAlgebra

for V being ComplexAlgebra st ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds

W is ComplexAlgebra

proof end;

theorem :: CC0SP1:16

for X being non empty set

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F

proof end;

theorem Th19: :: CC0SP1:19

for X being non empty set

for x being Element of X

for f being Function of X,COMPLEX

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds

|.(f . x).| <= ||.F.||

for x being Element of X

for f being Function of X,COMPLEX

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds

|.(f . x).| <= ||.F.||

proof end;

theorem :: CC0SP1:20

for X being non empty set

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

proof end;

theorem Th21: :: CC0SP1:21

for X being non empty set

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds

0 = ||.F.||

for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds

0 = ||.F.||

proof end;

theorem Th22: :: CC0SP1:22

for X being non empty set

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th23: :: CC0SP1:23

for X being non empty set

for a being Complex

for f, g being Function of X,COMPLEX

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for a being Complex

for f, g being Function of X,COMPLEX

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th24: :: CC0SP1:24

for X being non empty set

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th25: :: CC0SP1:25

for X being non empty set

for a being Complex

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

for a being Complex

for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof 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;

registration

let X be non empty set ;

( C_Normed_Algebra_of_BoundedFunctions X is right_complementable & C_Normed_Algebra_of_BoundedFunctions X is Abelian & C_Normed_Algebra_of_BoundedFunctions X is add-associative & C_Normed_Algebra_of_BoundedFunctions X is right_zeroed & C_Normed_Algebra_of_BoundedFunctions X is vector-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-associative & C_Normed_Algebra_of_BoundedFunctions X is scalar-unital & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by Th17, Lm4;

end;
cluster C_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;

coherence ( C_Normed_Algebra_of_BoundedFunctions X is right_complementable & C_Normed_Algebra_of_BoundedFunctions X is Abelian & C_Normed_Algebra_of_BoundedFunctions X is add-associative & C_Normed_Algebra_of_BoundedFunctions X is right_zeroed & C_Normed_Algebra_of_BoundedFunctions X is vector-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & C_Normed_Algebra_of_BoundedFunctions X is scalar-associative & C_Normed_Algebra_of_BoundedFunctions X is scalar-unital & C_Normed_Algebra_of_BoundedFunctions X is discerning & C_Normed_Algebra_of_BoundedFunctions X is reflexive & C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by Th17, Lm4;

theorem Th26: :: CC0SP1:26

for X being non empty set

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

for f, g, h being Function of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

proof end;

theorem Th27: :: CC0SP1:27

for X being non empty set

for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds

seq is convergent

for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds

seq is convergent

proof end;

registration
end;