:: CFUNCDOM semantic presentation

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

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :

definition

let A be non empty set ;
func ComplexFuncZero A -> Element of Funcs A,COMPLEX equals :: CFUNCDOM:def 4
A --> 0;
coherence

proof end;

end;

:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :

definition

let A be non empty set ;
func ComplexFuncUnit A -> Element of Funcs A,COMPLEX equals :: CFUNCDOM:def 5
A --> 1r ;
coherence

proof end;

end;

:: 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

proof end;

theorem Th1: :: CFUNCDOM:1

for A being non empty set
for h, f, g 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 h, f, g 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 Th3: :: CFUNCDOM:3

for A being non empty set
for x being Element of A holds (ComplexFuncUnit A) . x = 1r by FUNCOP_1:13;

theorem Th4: :: CFUNCDOM:4

for A being non empty set
for x being Element of A holds (ComplexFuncZero A) . x = 0 by FUNCOP_1:13;

theorem :: CFUNCDOM:5

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

proof end;

theorem Th6: :: CFUNCDOM:6

for A being non empty set
for h, f 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 Th7: :: CFUNCDOM:7

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 Th8: :: CFUNCDOM:8

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 Th9: :: CFUNCDOM:9

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 Th10: :: CFUNCDOM:10

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 Th11: :: CFUNCDOM:11

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

proof end;

theorem Th12: :: CFUNCDOM:12

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

proof end;

theorem Th13: :: CFUNCDOM:13

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 Th14: :: CFUNCDOM:14

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

proof end;

theorem Th15: :: CFUNCDOM:15

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 Th16: :: CFUNCDOM:16

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 Th17: :: CFUNCDOM:17

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 Th18: :: CFUNCDOM:18

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 Th19: :: CFUNCDOM:19

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 Th20: :: CFUNCDOM:20

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:21

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 Th22: :: CFUNCDOM:22

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:23

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 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]) ) )

proof end;

theorem Th25: :: CFUNCDOM:25

for A being non empty set holds CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace

proof end;

definition

let A be non empty set ;
func ComplexVectSpace A -> strict ComplexLinearSpace equals :: CFUNCDOM:def 6
CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);
coherence by Th25;

end;

:: deftheorem defines ComplexVectSpace CFUNCDOM:def 6 :

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

proof end;

theorem :: CFUNCDOM:26

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 -> strict doubleLoopStr equals :: CFUNCDOM:def 7
doubleLoopStr(# (Funcs A,COMPLEX ),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);
correctness ;

end;

:: deftheorem defines CRing CFUNCDOM:def 7 :

registration

let A be non empty set ;
cluster CRing A -> non empty strict ;
coherence

proof end;

end;

Lm4: for A being non empty set
for x, y being Element of (CRing A) holds x * y = y * x
by Th9;

Lm5: now

let A be non empty set ; :: thesis:
let x, e be Element of (CRing A); :: thesis:
assume A1: e = ComplexFuncUnit A ; :: thesis:
reconsider a = x as Element of Funcs A,COMPLEX ;
thus A2: e * x = the mult of (CRing A) . e,x
.= (ComplexFuncMult A) . (ComplexFuncUnit A),a by A1
.= x by Th11 ; :: thesis:
thus x * e = e * x by Lm4
.= x by A2 ; :: thesis:

end;

registration

let A be non empty set ;
cluster CRing A -> non empty unital strict ;
coherence

proof end;

end;

Lm6: now

let A be non empty set ; :: thesis:
reconsider e = ComplexFuncUnit A as Element of (CRing A) ;
for x being Element of (CRing A) holds
( x * e = x & e * x = x ) by Lm5;
hence 1. (CRing A) = ComplexFuncUnit A by GROUP_1:def 5; :: thesis:

end;

theorem Th27: :: CFUNCDOM:27

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 & ex t being Element of (CRing A) st x + t = 0. (CRing A) & 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:28

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, mult, add, Mult, unity, Zero #) -> ComplexAlgebraStr ;

end;

registration

cluster non empty ComplexAlgebraStr ;
existence

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 ;

end;

:: deftheorem defines CAlgebra CFUNCDOM:def 8 :

registration

let A be non empty set ;
cluster CAlgebra A -> non empty strict ;
coherence

proof end;

end;

Lm7: for A being non empty set
for x, y being Element of (CAlgebra A) holds x * y = y * x
by Th9;

Lm8: now

let A be non empty set ; :: thesis:
let x, e be Element of (CAlgebra A); :: thesis:
assume A1: e = ComplexFuncUnit A ; :: thesis:
reconsider a = x as Element of Funcs A,COMPLEX ;
thus A2: e * x = the mult of (CAlgebra A) . e,x
.= (ComplexFuncMult A) . (ComplexFuncUnit A),a by A1
.= x by Th11 ; :: thesis:
thus x * e = e * x by Lm7
.= x by A2 ; :: thesis:

end;

registration

let A be non empty set ;
cluster CAlgebra A -> non empty unital strict ;
coherence

proof end;

end;

Lm9: now

let A be non empty set ; :: thesis:
reconsider e = ComplexFuncUnit A as Element of (CAlgebra A) ;
for x being Element of (CAlgebra A) holds
( x * e = x & e * x = x ) by Lm8;
hence 1. (CAlgebra A) = ComplexFuncUnit A by GROUP_1:def 5; :: thesis:

end;

theorem Th29: :: CFUNCDOM:29

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 & ex t being Element of (CAlgebra A) st x + t = 0. (CAlgebra A) & 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 ComplexAlgebra-like means :Def9: :: CFUNCDOM:def 9
for x, y, z being Element of IT
for a, b being Complex holds
( x * (1. IT) = 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) );

end;

:: deftheorem Def9 defines ComplexAlgebra-like CFUNCDOM:def 9 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict ComplexAlgebra-like ComplexAlgebraStr ;
existence

proof end;

end;

definition

mode ComplexAlgebra is non empty Abelian add-associative right_zeroed right_complementable associative commutative ComplexAlgebra-like ComplexAlgebraStr ;

end;

theorem :: CFUNCDOM:30

for A being non empty set holds CAlgebra A is ComplexAlgebra

proof end;

theorem :: CFUNCDOM:31

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

theorem :: CFUNCDOM:32

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