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 :
for A being non empty set
for b2 being BinOp of (Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncAdd A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = addcomplex .: (f,g) );
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 :
for A being non empty set
for b2 being BinOp of (Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = multcomplex .: (f,g) );
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 :
for A being non empty set
for b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncExtMult A iff 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) );
:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :
for A being non empty set holds ComplexFuncZero A = A --> 0;
:: 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
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 :
for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);
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 :
for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);
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 :
for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);
theorem
:: 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 );
theorem
theorem
theorem