:: COMPLSP2 semantic presentation

definition

let c₁ be FinSequence of COMPLEX ;
func c₁ *' -> FinSequence of COMPLEX means :Def1: :: COMPLSP2:def 1
( len a₂ = len a₁ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₁ holds
a₂ . b₁ = (a₁ . b₁) *' ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines *' COMPLSP2:def 1 :

Lemma2: for b₁ being FinSequence of COMPLEX
for b₂ being Element of COMPLEX holds b₂ * b₁ = (multcomplex [;] b₂,(id COMPLEX )) * b₁

proof end;

theorem Th1: :: COMPLSP2:1

for b₁ being Nat
for b₂, b₃ being FinSequence of COMPLEX st b₁ in dom (b₂ + b₃) holds
(b₂ + b₃) . b₁ = (b₂ . b₁) + (b₃ . b₁)

proof end;

theorem Th2: :: COMPLSP2:2

for b₁ being Nat
for b₂, b₃ being FinSequence of COMPLEX st b₁ in dom (b₂ - b₃) holds
(b₂ - b₃) . b₁ = (b₂ . b₁) - (b₃ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on COMPLEX ;
redefine func - as c₂ - c₃ -> Element of a₁ -tuples_on COMPLEX ;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on COMPLEX ;
redefine func + as c₂ + c₃ -> Element of a₁ -tuples_on COMPLEX ;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be complex number ;
let c₃ be Element of c₁ -tuples_on COMPLEX ;
redefine func * as c₂ * c₃ -> Element of a₁ -tuples_on COMPLEX ;
coherence

proof end;

end;

theorem Th3: :: COMPLSP2:3

for b₁ being complex number
for b₂ being FinSequence of COMPLEX holds len (b₁ * b₂) = len b₂

proof end;

theorem Th4: :: COMPLSP2:4

for b₁ being FinSequence of COMPLEX holds dom b₁ = dom (- b₁)

proof end;

theorem Th5: :: COMPLSP2:5

for b₁ being FinSequence of COMPLEX holds len (- b₁) = len b₁

proof end;

theorem Th6: :: COMPLSP2:6

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
len (b₁ + b₂) = len b₁

proof end;

theorem Th7: :: COMPLSP2:7

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
len (b₁ - b₂) = len b₁

proof end;

theorem Th8: :: COMPLSP2:8

for b₁ being FinSequence of COMPLEX holds b₁ is Element of COMPLEX (len b₁)

proof end;

theorem Th9: :: COMPLSP2:9

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on COMPLEX holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th10: :: COMPLSP2:10

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
b₁ - b₂ = b₁ + (- b₂)

proof end;

theorem Th11: :: COMPLSP2:11

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on COMPLEX holds (- 1) * b₂ = - b₂

proof end;

theorem Th12: :: COMPLSP2:12

for b₁ being FinSequence of COMPLEX holds (- 1) * b₁ = - b₁

proof end;

theorem Th13: :: COMPLSP2:13

for b₁ being Nat
for b₂ being FinSequence of COMPLEX holds (- b₂) . b₁ = - (b₂ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂ be Element of c₁ -tuples_on COMPLEX ;
redefine func - as - c₂ -> Element of a₁ -tuples_on COMPLEX ;
coherence

proof end;

end;

theorem Th14: :: COMPLSP2:14

for b₁, b₂ being Nat
for b₃ being Element of COMPLEX
for b₄ being Element of b₁ -tuples_on COMPLEX st b₃ = b₄ . b₂ holds
(- b₄) . b₂ = - b₃ by Th13;

theorem Th15: :: COMPLSP2:15

for b₁ being FinSequence of COMPLEX
for b₂ being complex number holds dom (b₂ * b₁) = dom b₁

proof end;

theorem Th16: :: COMPLSP2:16

for b₁ being Nat
for b₂ being FinSequence of COMPLEX
for b₃ being complex number holds (b₃ * b₂) . b₁ = b₃ * (b₂ . b₁)

proof end;

theorem Th17: :: COMPLSP2:17

for b₁ being FinSequence of COMPLEX
for b₂ being complex number holds (b₂ * b₁) *' = (b₂ *' ) * (b₁ *' )

proof end;

theorem Th18: :: COMPLSP2:18

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on COMPLEX holds (b₃ + b₄) . b₂ = (b₃ . b₂) + (b₄ . b₂)

proof end;

theorem Th19: :: COMPLSP2:19

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
(b₁ + b₂) *' = (b₁ *' ) + (b₂ *' )

proof end;

theorem Th20: :: COMPLSP2:20

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on COMPLEX holds (b₃ - b₄) . b₂ = (b₃ . b₂) - (b₄ . b₂)

proof end;

theorem Th21: :: COMPLSP2:21

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
(b₁ - b₂) *' = (b₁ *' ) - (b₂ *' )

proof end;

theorem Th22: :: COMPLSP2:22

for b₁ being FinSequence of COMPLEX holds (b₁ *' ) *' = b₁

proof end;

theorem Th23: :: COMPLSP2:23

for b₁ being FinSequence of COMPLEX holds (- b₁) *' = - (b₁ *' )

proof end;

theorem Th24: :: COMPLSP2:24

for b₁ being complex number holds b₁ + (b₁ *' ) = 2 * (Re b₁)

proof end;

theorem Th25: :: COMPLSP2:25

for b₁ being Nat
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
(b₂ - b₃) . b₁ = (b₂ . b₁) - (b₃ . b₁)

proof end;

theorem Th26: :: COMPLSP2:26

for b₁ being Nat
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
(b₂ + b₃) . b₁ = (b₂ . b₁) + (b₃ . b₁)

proof end;

definition

let c₁ be FinSequence of COMPLEX ;
func Re c₁ -> FinSequence of REAL equals :: COMPLSP2:def 2
(1 / 2) * (a₁ + (a₁ *' ));
coherence

proof end;

end;

:: deftheorem Def2 defines Re COMPLSP2:def 2 :

theorem Th27: :: COMPLSP2:27

for b₁ being complex number holds b₁ - (b₁ *' ) = (2 * (Im b₁)) *

proof end;

definition

let c₁ be FinSequence of COMPLEX ;
func Im c₁ -> FinSequence of REAL equals :: COMPLSP2:def 3
(- ((1 / 2) * )) * (a₁ - (a₁ *' ));
coherence

proof end;

end;

:: deftheorem Def3 defines Im COMPLSP2:def 3 :

definition

end;

:: deftheorem Def4 defines |( COMPLSP2:def 4 :

theorem Th28: :: COMPLSP2:28

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
b₁ + (b₂ + b₃) = (b₁ + b₂) + b₃

proof end;

theorem Th29: :: COMPLSP2:29

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
b₁ + b₂ = b₂ + b₁

proof end;

theorem Th30: :: COMPLSP2:30

for b₁ being complex number
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof end;

theorem Th31: :: COMPLSP2:31

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
b₁ - b₂ = b₁ + (- b₂)

proof end;

definition

let c₁ be Nat;
let c₂ be Element of COMPLEX ;
redefine func |-> as c₁ |-> c₂ -> Element of a₁ -tuples_on COMPLEX ;
coherence by FINSEQ_2:132;

end;

theorem Th32: :: COMPLSP2:32

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ & b₁ + b₂ = 0c (len b₁) holds
( b₁ = - b₂ & b₂ = - b₁ )

proof end;

theorem Th33: :: COMPLSP2:33

for b₁ being FinSequence of COMPLEX holds b₁ + (0c (len b₁)) = b₁

proof end;

theorem Th34: :: COMPLSP2:34

for b₁ being FinSequence of COMPLEX holds b₁ + (- b₁) = 0c (len b₁)

proof end;

theorem Th35: :: COMPLSP2:35

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
- (b₁ + b₂) = (- b₁) + (- b₂)

proof end;

theorem Th36: :: COMPLSP2:36

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
(b₁ - b₂) - b₃ = b₁ - (b₂ + b₃)

proof end;

theorem Th37: :: COMPLSP2:37

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
b₁ + (b₂ - b₃) = (b₁ + b₂) - b₃

proof end;

theorem Th38: :: COMPLSP2:38

for b₁ being FinSequence of COMPLEX holds - (- b₁) = b₁

proof end;

theorem Th39: :: COMPLSP2:39

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
- (b₁ - b₂) = (- b₁) + b₂

proof end;

theorem Th40: :: COMPLSP2:40

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
b₁ - (b₂ - b₃) = (b₁ - b₂) + b₃

proof end;

theorem Th41: :: COMPLSP2:41

for b₁ being FinSequence of COMPLEX
for b₂ being complex number holds b₂ * (0c (len b₁)) = 0c (len b₁)

proof end;

theorem Th42: :: COMPLSP2:42

for b₁ being FinSequence of COMPLEX
for b₂ being complex number holds - (b₂ * b₁) = b₂ * (- b₁)

proof end;

theorem Th43: :: COMPLSP2:43

for b₁ being complex number
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
b₁ * (b₂ - b₃) = (b₁ * b₂) - (b₁ * b₃)

proof end;

theorem Th44: :: COMPLSP2:44

for b₁, b₂ being Element of COMPLEX
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
addcomplex . b₁,b₂ = addreal . b₃,b₄

proof end;

theorem Th45: :: COMPLSP2:45

for b₁ being Function of [:COMPLEX ,COMPLEX :], COMPLEX
for b₂ being Function of [:REAL ,REAL :], REAL
for b₃, b₄ being FinSequence of COMPLEX
for b₅, b₆ being FinSequence of REAL st b₃ = b₅ & b₄ = b₆ & len b₃ = len b₆ & ( for b₇ being Nat st b₇ in dom b₃ holds
b₁ . (b₃ . b₇),(b₄ . b₇) = b₂ . (b₅ . b₇),(b₆ . b₇) ) holds
b₁ .: b₃,b₄ = b₂ .: b₅,b₆

proof end;

Lemma44: 0 = 0c
;

definition

let c₁ be FinSequence of REAL ;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Element of REAL ;
coherence

proof end;

end;

theorem Th46: :: COMPLSP2:46

for b₁, b₂ being FinSequence of COMPLEX
for b₃, b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₁ = len b₄ holds
addcomplex .: b₁,b₂ = addreal .: b₃,b₄

proof end;

theorem Th47: :: COMPLSP2:47

for b₁, b₂ being FinSequence of COMPLEX
for b₃, b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₁ = len b₄ holds
b₁ + b₂ = b₃ + b₄

proof end;

theorem Th48: :: COMPLSP2:48

for b₁ being FinSequence of COMPLEX holds
( len (Re b₁) = len b₁ & len (Im b₁) = len b₁ )

proof end;

theorem Th49: :: COMPLSP2:49

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
( Re (b₁ + b₂) = (Re b₁) + (Re b₂) & Im (b₁ + b₂) = (Im b₁) + (Im b₂) )

proof end;

theorem Th50: :: COMPLSP2:50

for b₁, b₂ being FinSequence of COMPLEX
for b₃, b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₁ = len b₄ holds
diffcomplex .: b₁,b₂ = diffreal .: b₃,b₄

proof end;

theorem Th51: :: COMPLSP2:51

for b₁, b₂ being FinSequence of COMPLEX
for b₃, b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₁ = len b₄ holds
b₁ - b₂ = b₃ - b₄

proof end;

theorem Th52: :: COMPLSP2:52

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
( Re (b₁ - b₂) = (Re b₁) - (Re b₂) & Im (b₁ - b₂) = (Im b₁) - (Im b₂) )

proof end;

theorem Th53: :: COMPLSP2:53

for b₁ being FinSequence of COMPLEX
for b₂, b₃ being complex number holds b₂ * (b₃ * b₁) = (b₂ * b₃) * b₁

proof end;

Lemma53: for b₁ being FinSequence of COMPLEX holds - (0c (len b₁)) = 0c (len b₁)

proof end;

theorem Th54: :: COMPLSP2:54

for b₁ being FinSequence of COMPLEX
for b₂ being complex number holds (- b₂) * b₁ = - (b₂ * b₁)

proof end;

theorem Th55: :: COMPLSP2:55

for b₁ being Function of COMPLEX , COMPLEX
for b₂ being Function of REAL , REAL
for b₃ being FinSequence of COMPLEX
for b₄ being FinSequence of REAL st len b₃ = len b₄ & ( for b₅ being Nat st b₅ in dom b₃ holds
b₁ . (b₃ . b₅) = b₂ . (b₄ . b₅) ) holds
b₁ * b₃ = b₂ * b₄

proof end;

theorem Th56: :: COMPLSP2:56

for b₁ being FinSequence of COMPLEX
for b₂ being FinSequence of REAL st b₁ = b₂ & len b₁ = len b₂ holds
compcomplex * b₁ = compreal * b₂

proof end;

theorem Th57: :: COMPLSP2:57

for b₁ being FinSequence of COMPLEX
for b₂ being FinSequence of REAL st b₁ = b₂ & len b₁ = len b₂ holds
- b₁ = - b₂

proof end;

theorem Th58: :: COMPLSP2:58

for b₁ being FinSequence of COMPLEX holds
( Re ( * b₁) = - (Im b₁) & Im ( * b₁) = Re b₁ )

proof end;

theorem Th59: :: COMPLSP2:59

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|(( * b₁),b₂)| = * |(b₁,b₂)|

proof end;

theorem Th60: :: COMPLSP2:60

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|(b₁,( * b₂))| = - ( * |(b₁,b₂)|)

proof end;

theorem Th61: :: COMPLSP2:61

for b₁ being Element of COMPLEX
for b₂ being FinSequence of COMPLEX
for b₃ being Element of REAL
for b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₂ = len b₄ holds
(b₁ multcomplex ) * b₂ = (b₃ multreal ) * b₄

proof end;

theorem Th62: :: COMPLSP2:62

for b₁ being complex number
for b₂ being FinSequence of COMPLEX
for b₃ being Element of REAL
for b₄ being FinSequence of REAL st b₁ = b₃ & b₂ = b₄ & len b₂ = len b₄ holds
b₁ * b₂ = b₃ * b₄

proof end;

theorem Th63: :: COMPLSP2:63

for b₁ being FinSequence of COMPLEX
for b₂, b₃ being complex number holds (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁)

proof end;

theorem Th64: :: COMPLSP2:64

for b₁ being FinSequence of COMPLEX
for b₂, b₃ being complex number holds (b₂ - b₃) * b₁ = (b₂ * b₁) - (b₃ * b₁)

proof end;

theorem Th65: :: COMPLSP2:65

for b₁ being Element of COMPLEX
for b₂ being FinSequence of COMPLEX holds
( Re (b₁ * b₂) = ((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂)) & Im (b₁ * b₂) = ((Im b₁) * (Re b₂)) + ((Re b₁) * (Im b₂)) )

proof end;

theorem Th66: :: COMPLSP2:66

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
|((b₁ + b₂),b₃)| = |(b₁,b₃)| + |(b₂,b₃)|

proof end;

theorem Th67: :: COMPLSP2:67

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|((- b₁),b₂)| = - |(b₁,b₂)|

proof end;

theorem Th68: :: COMPLSP2:68

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|(b₁,(- b₂))| = - |(b₁,b₂)|

proof end;

theorem Th69: :: COMPLSP2:69

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|((- b₁),(- b₂))| = |(b₁,b₂)|

proof end;

theorem Th70: :: COMPLSP2:70

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
|((b₁ - b₂),b₃)| = |(b₁,b₃)| - |(b₂,b₃)|

proof end;

theorem Th71: :: COMPLSP2:71

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
|(b₁,(b₂ + b₃))| = |(b₁,b₂)| + |(b₁,b₃)|

proof end;

theorem Th72: :: COMPLSP2:72

for b₁, b₂, b₃ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ holds
|(b₁,(b₂ - b₃))| = |(b₁,b₂)| - |(b₁,b₃)|

proof end;

theorem Th73: :: COMPLSP2:73

for b₁, b₂, b₃, b₄ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ & len b₃ = len b₄ holds
|((b₁ + b₂),(b₃ + b₄))| = ((|(b₁,b₃)| + |(b₁,b₄)|) + |(b₂,b₃)|) + |(b₂,b₄)|

proof end;

theorem Th74: :: COMPLSP2:74

for b₁, b₂, b₃, b₄ being FinSequence of COMPLEX st len b₁ = len b₂ & len b₂ = len b₃ & len b₃ = len b₄ holds
|((b₁ - b₂),(b₃ - b₄))| = ((|(b₁,b₃)| - |(b₁,b₄)|) - |(b₂,b₃)|) + |(b₂,b₄)|

proof end;

theorem Th75: :: COMPLSP2:75

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|(b₁,b₂)| = |(b₂,b₁)| *'

proof end;

theorem Th76: :: COMPLSP2:76

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|((b₁ + b₂),(b₁ + b₂))| = (|(b₁,b₁)| + (2 * (Re |(b₁,b₂)|))) + |(b₂,b₂)|

proof end;

theorem Th77: :: COMPLSP2:77

for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len b₂ holds
|((b₁ - b₂),(b₁ - b₂))| = (|(b₁,b₁)| - (2 * (Re |(b₁,b₂)|))) + |(b₂,b₂)|

proof end;

theorem Th78: :: COMPLSP2:78

for b₁ being Element of COMPLEX
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
|((b₁ * b₂),b₃)| = b₁ * |(b₂,b₃)|

proof end;

theorem Th79: :: COMPLSP2:79

for b₁ being Element of COMPLEX
for b₂, b₃ being FinSequence of COMPLEX st len b₂ = len b₃ holds
|(b₂,(b₁ * b₃))| = (b₁ *' ) * |(b₂,b₃)|

proof end;

theorem Th80: :: COMPLSP2:80

for b₁, b₂ being Element of COMPLEX
for b₃, b₄, b₅ being FinSequence of COMPLEX st len b₃ = len b₄ & len b₄ = len b₅ holds
|(((b₁ * b₃) + (b₂ * b₄)),b₅)| = (b₁ * |(b₃,b₅)|) + (b₂ * |(b₄,b₅)|)

proof end;

theorem Th81: :: COMPLSP2:81

for b₁, b₂ being Element of COMPLEX
for b₃, b₄, b₅ being FinSequence of COMPLEX st len b₃ = len b₄ & len b₄ = len b₅ holds
|(b₃,((b₁ * b₄) + (b₂ * b₅)))| = ((b₁ *' ) * |(b₃,b₄)|) + ((b₂ *' ) * |(b₃,b₅)|)

proof end;