:: Complex Valued Function's Space
:: by Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
definition
let A be non
empty 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 b1 being BinOp of Funcs A,COMPLEX st
for f, g being Element of Funcs A,COMPLEX holds b1 . f,g = addcomplex .: f,g
uniqueness
for b1, b2 being BinOp of Funcs A,COMPLEX st ( for f, g being Element of Funcs A,COMPLEX holds b1 . f,g = addcomplex .: f,g ) & ( for f, g being Element of Funcs A,COMPLEX holds b2 . f,g = addcomplex .: f,g ) holds
b1 = b2
end;
:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def 1 :
definition
let A be non
empty 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 b1 being BinOp of Funcs A,COMPLEX st
for f, g being Element of Funcs A,COMPLEX holds b1 . f,g = multcomplex .: f,g
uniqueness
for b1, b2 being BinOp of Funcs A,COMPLEX st ( for f, g being Element of Funcs A,COMPLEX holds b1 . f,g = multcomplex .: f,g ) & ( for f, g being Element of Funcs A,COMPLEX holds b2 . f,g = multcomplex .: f,g ) holds
b1 = b2
end;
:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :
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 b1 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 (b1 . [z,f]) . x = z * (f . x)
uniqueness
for b1, b2 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 (b1 . [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 (b2 . [z,f]) . x = z * (f . x) ) holds
b1 = b2
end;
:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :
:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :
:: deftheorem defines ComplexFuncUnit CFUNCDOM:def 5 :
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
theorem Th1: :: CFUNCDOM:1
theorem Th2: :: CFUNCDOM:2
theorem :: CFUNCDOM:3
canceled;
theorem :: CFUNCDOM:4
canceled;
theorem :: CFUNCDOM:5
theorem Th6: :: CFUNCDOM:6
theorem Th7: :: CFUNCDOM:7
theorem Th8: :: CFUNCDOM:8
theorem Th9: :: CFUNCDOM:9
theorem Th10: :: CFUNCDOM:10
theorem Th11: :: CFUNCDOM:11
theorem Th12: :: CFUNCDOM:12
theorem Th13: :: CFUNCDOM:13
theorem Th14: :: CFUNCDOM:14
theorem Th15: :: CFUNCDOM:15
theorem Th16: :: CFUNCDOM:16
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)]
theorem Th17: :: CFUNCDOM:17
theorem Th18: :: CFUNCDOM:18
theorem Th19: :: CFUNCDOM:19
theorem Th20: :: CFUNCDOM:20
theorem :: CFUNCDOM:21
theorem Th22: :: CFUNCDOM:22
theorem :: CFUNCDOM:23
theorem Th24: :: CFUNCDOM:24
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]) ) )
theorem Th25: :: CFUNCDOM:25
:: deftheorem defines ComplexVectSpace CFUNCDOM:def 6 :
Lm3:
ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
theorem :: CFUNCDOM:26
definition
let A be non
empty set ;
func CRing A -> strict 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 strict doubleLoopStr ;
;
end;
:: deftheorem defines CRing CFUNCDOM:def 7 :
theorem Th27: :: CFUNCDOM:27
theorem :: CFUNCDOM:28
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 :
theorem Th29: :: CFUNCDOM:29
:: deftheorem Def9 defines ComplexAlgebra-like CFUNCDOM:def 9 :
theorem :: CFUNCDOM:30
theorem :: CFUNCDOM:31
theorem :: CFUNCDOM:32