:: Complex Valued Function's Space
:: by Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let A be set ;

func ComplexFuncAdd A -> BinOp of (Funcs (A,COMPLEX)) means :Def1: :: CFUNCDOM:def 1
for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = addcomplex .: (f,g);

existence
ex b₁ being BinOp of (Funcs (A,COMPLEX)) st
for f, g being Element of Funcs (A,COMPLEX) holds b₁ . (f,g) = addcomplex .: (f,g)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b₁ . (f,g) = addcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b₂ . (f,g) = addcomplex .: (f,g) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def 1 :
for A being set
for b₂ being BinOp of (Funcs (A,COMPLEX)) holds
( b₂ = ComplexFuncAdd A iff for f, g being Element of Funcs (A,COMPLEX) holds b₂ . (f,g) = addcomplex .: (f,g) );

registration

let A be set ;

cluster ComplexFuncAdd A -> complex-functions-valued ;

coherence
ComplexFuncAdd A is complex-functions-valued ;

end;

definition

let A be set ;

func ComplexFuncMult A -> BinOp of (Funcs (A,COMPLEX)) means :Def2: :: CFUNCDOM:def 2
for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = multcomplex .: (f,g);

existence
ex b₁ being BinOp of (Funcs (A,COMPLEX)) st
for f, g being Element of Funcs (A,COMPLEX) holds b₁ . (f,g) = multcomplex .: (f,g)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b₁ . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b₂ . (f,g) = multcomplex .: (f,g) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :
for A being set
for b₂ being BinOp of (Funcs (A,COMPLEX)) holds
( b₂ = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b₂ . (f,g) = multcomplex .: (f,g) );

registration

let A be set ;

cluster ComplexFuncMult A -> complex-functions-valued ;

coherence
ComplexFuncMult A is complex-functions-valued ;

end;

definition

let A be non empty set ;

func ComplexFuncExtMult A -> Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) means :Def3: :: CFUNCDOM:def 3
for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it . [z,f]) . x = z * (f . x);

existence
ex b₁ being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st
for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b₁ . [z,f]) . x = z * (f . x)

proof end;

uniqueness
for b₁, b₂ being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st ( for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b₁ . [z,f]) . x = z * (f . x) ) & ( for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b₂ . [z,f]) . x = z * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :
for A being non empty set
for b₂ being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds
( b₂ = ComplexFuncExtMult A iff for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b₂ . [z,f]) . x = z * (f . x) );

registration

let A be non empty set ;

cluster ComplexFuncExtMult A -> complex-functions-valued ;

coherence
ComplexFuncExtMult A is complex-functions-valued ;

end;

definition

let A be non empty set ;

func ComplexFuncZero A -> Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 4
A --> 0;

coherence
A --> 0 is Element of Funcs (A,COMPLEX)

proof end;

end;

:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :
for A being non empty set holds ComplexFuncZero A = A --> 0;

definition

let A be non empty set ;

func ComplexFuncUnit A -> Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 5
A --> 1r;

coherence
A --> 1r is Element of Funcs (A,COMPLEX) by FUNCT_2:8;

end;

:: deftheorem defines ComplexFuncUnit CFUNCDOM:def 5 :
for A being non empty set holds ComplexFuncUnit A = A --> 1r;

Lm1: for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f

proof end;

theorem Th1: :: CFUNCDOM:1

for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )

proof end;

theorem Th2: :: CFUNCDOM:2

for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )

proof end;

theorem :: CFUNCDOM:3

for A being non empty set holds ComplexFuncZero A <> ComplexFuncUnit A

proof end;

theorem Th4: :: CFUNCDOM:4

for A being non empty set
for f, h being Element of Funcs (A,COMPLEX)
for a being Complex holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )

proof end;

theorem Th5: :: CFUNCDOM:5

for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)

proof end;

theorem Th6: :: CFUNCDOM:6

for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)

proof end;

theorem Th7: :: CFUNCDOM:7

for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)

proof end;

theorem Th8: :: CFUNCDOM:8

for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)

proof end;

theorem Th9: :: CFUNCDOM:9

for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f

proof end;

theorem Th10: :: CFUNCDOM:10

for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f

proof end;

theorem Th11: :: CFUNCDOM:11

for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A

proof end;

theorem Th12: :: CFUNCDOM:12

for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f

proof end;

theorem Th13: :: CFUNCDOM:13

for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

proof end;

theorem Th14: :: CFUNCDOM:14

for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]

proof end;

Lm2: for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]

proof end;

theorem Th15: :: CFUNCDOM:15

for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))

proof end;

theorem Th16: :: CFUNCDOM:16

for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]

proof end;

theorem Th17: :: CFUNCDOM:17

for x1 being set
for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )

proof end;

theorem Th18: :: CFUNCDOM:18

for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )

proof end;

theorem :: CFUNCDOM:19

for x1, x2 being set
for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )

proof end;

theorem Th20: :: CFUNCDOM:20

for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

proof end;

theorem :: CFUNCDOM:21

for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

proof end;

theorem Th22: :: CFUNCDOM:22

for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )

proof end;

definition

let A be non empty set ;

func ComplexVectSpace A -> non empty strict CLSStruct equals :: CFUNCDOM:def 6
CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

coherence
CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is non empty strict CLSStruct ;

end;

:: deftheorem defines ComplexVectSpace CFUNCDOM:def 6 :
for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

registration

let A be non empty set ;

cluster ComplexVectSpace A -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for non empty strict CLSStruct ;

coherence
for b₁ being non empty strict CLSStruct st b₁ = ComplexVectSpace A holds
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is scalar-unital )

proof end;

end;

Lm3: ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )

proof end;

theorem :: CFUNCDOM:23

ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st
( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )

proof end;

definition

let A be non empty set ;

func CRing A -> doubleLoopStr equals :: CFUNCDOM:def 7
doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

correctness
coherence
doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is doubleLoopStr ;
;

end;

:: deftheorem defines CRing CFUNCDOM:def 7 :
for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

registration

let A be non empty set ;

cluster CRing A -> non empty strict ;

coherence
( not CRing A is empty & CRing A is strict ) ;

end;

Lm4: now :: thesis: for A being non empty set
for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )

let A be non empty set ; :: thesis: for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let x, e be Element of (CRing A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )
assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )
hence e * x = x by Th9; :: thesis: x * e = x
hence x * e = x by Th7; :: thesis: verum

end;

registration

let A be non empty set ;

cluster CRing A -> unital ;

coherence
CRing A is unital

proof end;

end;

theorem Th24: :: CFUNCDOM:24

for A being non empty set
for x, y, z being Element of (CRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

proof end;

theorem :: CFUNCDOM:25

for A being non empty set holds CRing A is commutative Ring

proof end;

definition

attr c₁ is strict ;
struct ComplexAlgebraStr -> doubleLoopStr , CLSStruct ;
aggr ComplexAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> ComplexAlgebraStr ;

end;

registration

cluster non empty for ComplexAlgebraStr ;

existence
not for b₁ being ComplexAlgebraStr holds b₁ is empty

proof end;

end;

definition

let A be non empty set ;

func CAlgebra A -> strict ComplexAlgebraStr equals :: CFUNCDOM:def 8
ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

correctness
coherence
ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is strict ComplexAlgebraStr ;
;

end;

:: deftheorem defines CAlgebra CFUNCDOM:def 8 :
for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

registration

let A be non empty set ;

cluster CAlgebra A -> non empty strict ;

coherence
not CAlgebra A is empty ;

end;

Lm5: now :: thesis: for A being non empty set
for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )

let A be non empty set ; :: thesis: for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let x, e be Element of (CAlgebra A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )
assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )
hence e * x = x by Th9; :: thesis: x * e = x
hence x * e = x by Th7; :: thesis: verum

end;

registration

let A be non empty set ;

cluster CAlgebra A -> unital strict ;

coherence
CAlgebra A is unital

proof end;

end;

theorem :: CFUNCDOM:26

for A being non empty set
for x, y, z being Element of (CAlgebra A)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )

proof end;

definition

let IT be non empty ComplexAlgebraStr ;

attr IT is vector-associative means :: CFUNCDOM:def 9
for x, y being Element of IT
for a being Complex holds a * (x * y) = (a * x) * y;

end;

:: deftheorem defines vector-associative CFUNCDOM:def 9 :
for IT being non empty ComplexAlgebraStr holds
( IT is vector-associative iff for x, y being Element of IT
for a being Complex holds a * (x * y) = (a * x) * y );

registration

let A be non empty set ;

cluster CAlgebra A -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative strict vector-associative ;

coherence
( CAlgebra A is strict & CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

proof end;

end;

registration

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative strict vector-associative for ComplexAlgebraStr ;

existence
ex b₁ being non empty ComplexAlgebraStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is commutative & b₁ is associative & b₁ is right_unital & b₁ is right-distributive & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is vector-associative )

proof end;

end;

definition

mode ComplexAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative vector-associative ComplexAlgebraStr ;

end;

theorem :: CFUNCDOM:27

for A being non empty set holds CAlgebra A is ComplexAlgebra ;

theorem :: CFUNCDOM:28

for A being non empty set holds 1. (CRing A) = ComplexFuncUnit A ;

theorem :: CFUNCDOM:29

for A being non empty set holds 1. (CAlgebra A) = ComplexFuncUnit A ;