begin
definition
let A be non
empty set ;
func ComplexFuncAdd A -> BinOp of
(Funcs A,COMPLEX ) means :
Def1:
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:
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:
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:
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
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:
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
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:
:: 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
definition
let A be non
empty set ;
func CRing A -> doubleLoopStr equals
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 :
theorem Th27:
theorem
definition
let A be non
empty set ;
func CAlgebra A -> strict ComplexAlgebraStr equals
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
:: deftheorem defines vector-associative CFUNCDOM:def 9 :
theorem
theorem
theorem