:: CFUNCDOM semantic presentation

definition

let c₁ be non empty set ;
func ComplexFuncAdd c₁ -> BinOp of Funcs a₁,COMPLEX means :Def1: :: CFUNCDOM:def 1
for b₁, b₂ being Element of Funcs a₁,COMPLEX holds a₂ . b₁,b₂ = addcomplex .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def 1 :

definition

let c₁ be non empty set ;
func ComplexFuncMult c₁ -> BinOp of Funcs a₁,COMPLEX means :Def2: :: CFUNCDOM:def 2
for b₁, b₂ being Element of Funcs a₁,COMPLEX holds a₂ . b₁,b₂ = multcomplex .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :

definition

let c₁ be non empty set ;
func ComplexFuncExtMult c₁ -> Function of [:COMPLEX ,(Funcs a₁,COMPLEX ):], Funcs a₁,COMPLEX means :Def3: :: CFUNCDOM:def 3
for b₁ being Complex
for b₂ being Element of Funcs a₁,COMPLEX
for b₃ being Element of a₁ holds (a₂ . [b₁,b₂]) . b₃ = b₁ * (b₂ . b₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :

definition

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

proof end;

end;

:: deftheorem Def4 defines ComplexFuncZero CFUNCDOM:def 4 :

definition

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

proof end;

end;

:: deftheorem Def5 defines ComplexFuncUnit CFUNCDOM:def 5 :

Lemma4: for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Function of b₁,b₂ holds b₃ in dom b₄

proof end;

theorem Th1: :: CFUNCDOM:1

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,COMPLEX holds
( b₂ = (ComplexFuncAdd b₁) . b₃,b₄ iff for b₅ being Element of b₁ holds b₂ . b₅ = (b₃ . b₅) + (b₄ . b₅) )

proof end;

theorem Th2: :: CFUNCDOM:2

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,COMPLEX holds
( b₂ = (ComplexFuncMult b₁) . b₃,b₄ iff for b₅ being Element of b₁ holds b₂ . b₅ = (b₃ . b₅) * (b₄ . b₅) )

proof end;

theorem Th3: :: CFUNCDOM:3

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

theorem Th4: :: CFUNCDOM:4

for b₁ being non empty set
for b₂ being Element of b₁ holds (ComplexFuncZero b₁) . b₂ = 0 by FUNCOP_1:13;

theorem Th5: :: CFUNCDOM:5

for b₁ being non empty set holds ComplexFuncZero b₁ <> ComplexFuncUnit b₁

proof end;

theorem Th6: :: CFUNCDOM:6

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,COMPLEX
for b₄ being Complex holds
( b₂ = (ComplexFuncExtMult b₁) . [b₄,b₃] iff for b₅ being Element of b₁ holds b₂ . b₅ = b₄ * (b₃ . b₅) )

proof end;

theorem Th7: :: CFUNCDOM:7

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,COMPLEX holds (ComplexFuncAdd b₁) . b₂,b₃ = (ComplexFuncAdd b₁) . b₃,b₂

proof end;

theorem Th8: :: CFUNCDOM:8

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,COMPLEX holds (ComplexFuncAdd b₁) . b₂,((ComplexFuncAdd b₁) . b₃,b₄) = (ComplexFuncAdd b₁) . ((ComplexFuncAdd b₁) . b₂,b₃),b₄

proof end;

theorem Th9: :: CFUNCDOM:9

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,COMPLEX holds (ComplexFuncMult b₁) . b₂,b₃ = (ComplexFuncMult b₁) . b₃,b₂

proof end;

theorem Th10: :: CFUNCDOM:10

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,COMPLEX holds (ComplexFuncMult b₁) . b₂,((ComplexFuncMult b₁) . b₃,b₄) = (ComplexFuncMult b₁) . ((ComplexFuncMult b₁) . b₂,b₃),b₄

proof end;

theorem Th11: :: CFUNCDOM:11

for b₁ being non empty set
for b₂ being Element of Funcs b₁,COMPLEX holds (ComplexFuncMult b₁) . (ComplexFuncUnit b₁),b₂ = b₂

proof end;

theorem Th12: :: CFUNCDOM:12

for b₁ being non empty set
for b₂ being Element of Funcs b₁,COMPLEX holds (ComplexFuncAdd b₁) . (ComplexFuncZero b₁),b₂ = b₂

proof end;

theorem Th13: :: CFUNCDOM:13

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

proof end;

theorem Th14: :: CFUNCDOM:14

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

proof end;

theorem Th15: :: CFUNCDOM:15

for b₁ being non empty set
for b₂ being Element of Funcs b₁,COMPLEX
for b₃, b₄ being Complex holds (ComplexFuncExtMult b₁) . [b₃,((ComplexFuncExtMult b₁) . [b₄,b₂])] = (ComplexFuncExtMult b₁) . [(b₃ * b₄),b₂]

proof end;

theorem Th16: :: CFUNCDOM:16

for b₁ being non empty set
for b₂ being Element of Funcs b₁,COMPLEX
for b₃, b₄ being Complex holds (ComplexFuncAdd b₁) . ((ComplexFuncExtMult b₁) . [b₃,b₂]),((ComplexFuncExtMult b₁) . [b₄,b₂]) = (ComplexFuncExtMult b₁) . [(b₃ + b₄),b₂]

proof end;

Lemma20: for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,COMPLEX
for b₄ being Complex holds (ComplexFuncAdd b₁) . ((ComplexFuncExtMult b₁) . [b₄,b₂]),((ComplexFuncExtMult b₁) . [b₄,b₃]) = (ComplexFuncExtMult b₁) . [b₄,((ComplexFuncAdd b₁) . b₂,b₃)]

proof end;

theorem Th17: :: CFUNCDOM:17

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,COMPLEX holds (ComplexFuncMult b₁) . b₂,((ComplexFuncAdd b₁) . b₃,b₄) = (ComplexFuncAdd b₁) . ((ComplexFuncMult b₁) . b₂,b₃),((ComplexFuncMult b₁) . b₂,b₄)

proof end;

theorem Th18: :: CFUNCDOM:18

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,COMPLEX
for b₄ being Complex holds (ComplexFuncMult b₁) . ((ComplexFuncExtMult b₁) . [b₄,b₂]),b₃ = (ComplexFuncExtMult b₁) . [b₄,((ComplexFuncMult b₁) . b₂,b₃)]

proof end;

theorem Th19: :: CFUNCDOM:19

for b₁ being set
for b₂ being non empty set ex b₃, b₄ being Element of Funcs b₂,COMPLEX st
( ( for b₅ being set st b₅ in b₂ holds
( ( b₅ = b₁ implies b₃ . b₅ = 1r ) & ( b₅ <> b₁ implies b₃ . b₅ = 0 ) ) ) & ( for b₅ being set st b₅ in b₂ holds
( ( b₅ = b₁ implies b₄ . b₅ = 0 ) & ( b₅ <> b₁ implies b₄ . b₅ = 1r ) ) ) )

proof end;

theorem Th20: :: CFUNCDOM:20

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being Element of Funcs b₃,COMPLEX st b₁ in b₃ & b₂ in b₃ & b₁ <> b₂ & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₄ . b₆ = 1r ) & ( b₆ <> b₁ implies b₄ . b₆ = 0 ) ) ) & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₅ . b₆ = 0 ) & ( b₆ <> b₁ implies b₅ . b₆ = 1r ) ) ) holds
for b₆, b₇ being Complex st (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₆,b₄]),((ComplexFuncExtMult b₃) . [b₇,b₅]) = ComplexFuncZero b₃ holds
( b₆ = 0c & b₇ = 0c )

proof end;

theorem Th21: :: CFUNCDOM:21

for b₁, b₂ being set
for b₃ being non empty set st b₁ in b₃ & b₂ in b₃ & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,COMPLEX st
for b₆, b₇ being Complex st (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₆,b₄]),((ComplexFuncExtMult b₃) . [b₇,b₅]) = ComplexFuncZero b₃ holds
( b₆ = 0 & b₇ = 0 )

proof end;

theorem Th22: :: CFUNCDOM:22

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being Element of Funcs b₃,COMPLEX st b₃ = {b₁,b₂} & b₁ <> b₂ & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₄ . b₆ = 1r ) & ( b₆ <> b₁ implies b₄ . b₆ = 0 ) ) ) & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₅ . b₆ = 0 ) & ( b₆ <> b₁ implies b₅ . b₆ = 1r ) ) ) holds
for b₆ being Element of Funcs b₃,COMPLEX ex b₇, b₈ being Complex st b₆ = (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₇,b₄]),((ComplexFuncExtMult b₃) . [b₈,b₅])

proof end;

theorem Th23: :: CFUNCDOM:23

for b₁, b₂ being set
for b₃ being non empty set st b₃ = {b₁,b₂} & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,COMPLEX st
for b₆ being Element of Funcs b₃,COMPLEX ex b₇, b₈ being Complex st b₆ = (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₇,b₄]),((ComplexFuncExtMult b₃) . [b₈,b₅])

proof end;

theorem Th24: :: CFUNCDOM:24

for b₁, b₂ being set
for b₃ being non empty set st b₃ = {b₁,b₂} & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,COMPLEX st
( ( for b₆, b₇ being Complex st (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₆,b₄]),((ComplexFuncExtMult b₃) . [b₇,b₅]) = ComplexFuncZero b₃ holds
( b₆ = 0 & b₇ = 0 ) ) & ( for b₆ being Element of Funcs b₃,COMPLEX ex b₇, b₈ being Complex st b₆ = (ComplexFuncAdd b₃) . ((ComplexFuncExtMult b₃) . [b₇,b₄]),((ComplexFuncExtMult b₃) . [b₈,b₅]) ) )

proof end;

theorem Th25: :: CFUNCDOM:25

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

proof end;

definition

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

end;

:: deftheorem Def6 defines ComplexVectSpace CFUNCDOM:def 6 :

Lemma28: ex b₁ being non empty set ex b₂, b₃ being set st
( b₁ = {b₂,b₃} & b₂ <> b₃ )

proof end;

theorem Th26: :: CFUNCDOM:26

ex b₁ being strict ComplexLinearSpaceex b₂, b₃ being VECTOR of b₁ st
( ( for b₄, b₅ being Complex st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) ) & ( for b₄ being VECTOR of b₁ ex b₅, b₆ being Complex st b₄ = (b₅ * b₂) + (b₆ * b₃) ) )

proof end;

definition

let c₁ be non empty set ;
func CRing c₁ -> strict doubleLoopStr equals :: CFUNCDOM:def 7
doubleLoopStr(# (Funcs a₁,COMPLEX ),(ComplexFuncAdd a₁),(ComplexFuncMult a₁),(ComplexFuncUnit a₁),(ComplexFuncZero a₁) #);
correctness ;

end;

:: deftheorem Def7 defines CRing CFUNCDOM:def 7 :

registration

let c₁ be non empty set ;
cluster CRing a₁ -> non empty strict ;
coherence

proof end;

end;

Lemma29: for b₁ being non empty set
for b₂, b₃ being Element of (CRing b₁) holds b₂ * b₃ = b₃ * b₂
by Th9;

E30: now

let c₁ be non empty set ;
let c₂, c₃ be Element of (CRing c₁);
assume E31: c₃ = ComplexFuncUnit c₁ ;
reconsider c₄ = c₂ as Element of Funcs c₁,COMPLEX ;
thus E32: c₃ * c₂ = the mult of (CRing c₁) . c₃,c₂
.= (ComplexFuncMult c₁) . (ComplexFuncUnit c₁),c₄ by E31
.= c₂ by Th11 ;
thus c₂ * c₃ = c₃ * c₂ by Lemma29
.= c₂ by E32 ;

end;

registration

let c₁ be non empty set ;
cluster CRing a₁ -> non empty unital strict ;
coherence

proof end;

end;

E31: now

let c₁ be non empty set ;
reconsider c₂ = ComplexFuncUnit c₁ as Element of (CRing c₁) ;
for b₁ being Element of (CRing c₁) holds
( b₁ * c₂ = b₁ & c₂ * b₁ = b₁ ) by Lemma30;
hence 1. (CRing c₁) = ComplexFuncUnit c₁ by GROUP_1:def 5;

end;

theorem Th27: :: CFUNCDOM:27

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (CRing b₁) holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (CRing b₁)) = b₂ & ex b₅ being Element of (CRing b₁) st b₂ + b₅ = 0. (CRing b₁) & b₂ * b₃ = b₃ * b₂ & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (CRing b₁)) = b₂ & (1. (CRing b₁)) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) )

proof end;

theorem Th28: :: CFUNCDOM:28

for b₁ being non empty set holds CRing b₁ is commutative Ring

proof end;

definition

attr a₁ 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 c₁ be non empty set ;
func CAlgebra c₁ -> strict ComplexAlgebraStr equals :: CFUNCDOM:def 8
ComplexAlgebraStr(# (Funcs a₁,COMPLEX ),(ComplexFuncMult a₁),(ComplexFuncAdd a₁),(ComplexFuncExtMult a₁),(ComplexFuncUnit a₁),(ComplexFuncZero a₁) #);
correctness ;

end;

:: deftheorem Def8 defines CAlgebra CFUNCDOM:def 8 :

registration

let c₁ be non empty set ;
cluster CAlgebra a₁ -> non empty strict ;
coherence

proof end;

end;

Lemma33: for b₁ being non empty set
for b₂, b₃ being Element of (CAlgebra b₁) holds b₂ * b₃ = b₃ * b₂
by Th9;

E34: now

let c₁ be non empty set ;
let c₂, c₃ be Element of (CAlgebra c₁);
assume E35: c₃ = ComplexFuncUnit c₁ ;
reconsider c₄ = c₂ as Element of Funcs c₁,COMPLEX ;
thus E36: c₃ * c₂ = the mult of (CAlgebra c₁) . c₃,c₂
.= (ComplexFuncMult c₁) . (ComplexFuncUnit c₁),c₄ by E35
.= c₂ by Th11 ;
thus c₂ * c₃ = c₃ * c₂ by Lemma33
.= c₂ by E36 ;

end;

registration

let c₁ be non empty set ;
cluster CAlgebra a₁ -> non empty unital strict ;
coherence

proof end;

end;

E35: now

let c₁ be non empty set ;
reconsider c₂ = ComplexFuncUnit c₁ as Element of (CAlgebra c₁) ;
for b₁ being Element of (CAlgebra c₁) holds
( b₁ * c₂ = b₁ & c₂ * b₁ = b₁ ) by Lemma34;
hence 1. (CAlgebra c₁) = ComplexFuncUnit c₁ by GROUP_1:def 5;

end;

theorem Th29: :: CFUNCDOM:29

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (CAlgebra b₁)
for b₅, b₆ being Complex holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (CAlgebra b₁)) = b₂ & ex b₇ being Element of (CAlgebra b₁) st b₂ + b₇ = 0. (CAlgebra b₁) & b₂ * b₃ = b₃ * b₂ & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (CAlgebra b₁)) = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & b₅ * (b₂ * b₃) = (b₅ * b₂) * b₃ & b₅ * (b₂ + b₃) = (b₅ * b₂) + (b₅ * b₃) & (b₅ + b₆) * b₂ = (b₅ * b₂) + (b₆ * b₂) & (b₅ * b₆) * b₂ = b₅ * (b₆ * b₂) )

proof end;

definition

let c₁ be non empty ComplexAlgebraStr ;
attr a₁ is ComplexAlgebra-like means :Def9: :: CFUNCDOM:def 9
for b₁, b₂, b₃ being Element of a₁
for b₄, b₅ being Complex holds
( b₁ * (1. a₁) = b₁ & b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & b₄ * (b₁ * b₂) = (b₄ * b₁) * b₂ & b₄ * (b₁ + b₂) = (b₄ * b₁) + (b₄ * b₂) & (b₄ + b₅) * b₁ = (b₄ * b₁) + (b₅ * b₁) & (b₄ * b₅) * b₁ = b₄ * (b₅ * b₁) );

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 Th30: :: CFUNCDOM:30

for b₁ being non empty set holds CAlgebra b₁ is ComplexAlgebra

proof end;

theorem Th31: :: CFUNCDOM:31

for b₁ being non empty set holds 1. (CRing b₁) = ComplexFuncUnit b₁ by Lemma31;

theorem Th32: :: CFUNCDOM:32

for b₁ being non empty set holds 1. (CAlgebra b₁) = ComplexFuncUnit b₁ by Lemma35;