:: COMPLSP2 semantic presentation

definition

let z be FinSequence of COMPLEX ;
func z *' -> FinSequence of COMPLEX means :Def1: :: COMPLSP2:def 1
( len it = len z & ( for i being Nat st 1 <= i & i <= len z holds
it . i = (z . i) *' ) );
existence

proof end;

uniqueness

proof end;

end;

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

Lm1: for x being FinSequence of COMPLEX
for c being Element of COMPLEX holds c * x = (multcomplex [;] c,(id COMPLEX )) * x

proof end;

theorem Th1: :: COMPLSP2:1

for i being Nat
for x, y being FinSequence of COMPLEX st i in dom (x + y) holds
(x + y) . i = (x . i) + (y . i)

proof end;

theorem Th2: :: COMPLSP2:2

for i being Nat
for x, y being FinSequence of COMPLEX st i in dom (x - y) holds
(x - y) . i = (x . i) - (y . i)

proof end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on COMPLEX ;
:: original: -
redefine func R1 - R2 -> Element of i -tuples_on COMPLEX ;
coherence

proof end;

end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on COMPLEX ;
:: original: +
redefine func R1 + R2 -> Element of i -tuples_on COMPLEX ;
coherence

proof end;

end;

definition

let i be Nat;
let r be complex number ;
let R be Element of i -tuples_on COMPLEX ;
:: original: *
redefine func r * R -> Element of i -tuples_on COMPLEX ;
coherence

proof end;

end;

theorem Th3: :: COMPLSP2:3

for a being complex number
for x being FinSequence of COMPLEX holds len (a * x) = len x

proof end;

theorem Th4: :: COMPLSP2:4

for x being FinSequence of COMPLEX holds dom x = dom (- x)

proof end;

theorem Th5: :: COMPLSP2:5

for x being FinSequence of COMPLEX holds len (- x) = len x

proof end;

theorem Th6: :: COMPLSP2:6

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
len (x1 + x2) = len x1

proof end;

theorem Th7: :: COMPLSP2:7

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
len (x1 - x2) = len x1

proof end;

theorem Th8: :: COMPLSP2:8

for f being FinSequence of COMPLEX holds f is Element of COMPLEX (len f)

proof end;

theorem Th9: :: COMPLSP2:9

for i being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds R1 - R2 = R1 + (- R2)

proof end;

theorem Th10: :: COMPLSP2:10

for x, y being FinSequence of COMPLEX st len x = len y holds
x - y = x + (- y)

proof end;

theorem Th11: :: COMPLSP2:11

for i being Nat
for R being Element of i -tuples_on COMPLEX holds (- 1) * R = - R

proof end;

theorem Th12: :: COMPLSP2:12

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

proof end;

theorem Th13: :: COMPLSP2:13

for i being Nat
for x being FinSequence of COMPLEX holds (- x) . i = - (x . i)

proof end;

definition

let i be Nat;
let R be Element of i -tuples_on COMPLEX ;
:: original: -
redefine func - R -> Element of i -tuples_on COMPLEX ;
coherence

proof end;

end;

theorem :: COMPLSP2:14

for i, j being Nat
for c being Element of COMPLEX
for R being Element of i -tuples_on COMPLEX st c = R . j holds
(- R) . j = - c by Th13;

theorem Th15: :: COMPLSP2:15

for x being FinSequence of COMPLEX
for a being complex number holds dom (a * x) = dom x

proof end;

theorem Th16: :: COMPLSP2:16

for i being Nat
for x being FinSequence of COMPLEX
for a being complex number holds (a * x) . i = a * (x . i)

proof end;

theorem Th17: :: COMPLSP2:17

for x being FinSequence of COMPLEX
for a being complex number holds (a * x) *' = (a *' ) * (x *' )

proof end;

theorem Th18: :: COMPLSP2:18

for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 + R2) . j = (R1 . j) + (R2 . j)

proof end;

theorem Th19: :: COMPLSP2:19

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
(x1 + x2) *' = (x1 *' ) + (x2 *' )

proof end;

theorem Th20: :: COMPLSP2:20

for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)

proof end;

theorem Th21: :: COMPLSP2:21

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
(x1 - x2) *' = (x1 *' ) - (x2 *' )

proof end;

theorem :: COMPLSP2:22

for z being FinSequence of COMPLEX holds (z *' ) *' = z

proof end;

theorem :: COMPLSP2:23

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

proof end;

theorem Th24: :: COMPLSP2:24

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

proof end;

theorem Th25: :: COMPLSP2:25

for i being Nat
for x, y being FinSequence of COMPLEX st len x = len y holds
(x - y) . i = (x . i) - (y . i)

proof end;

theorem Th26: :: COMPLSP2:26

for i being Nat
for x, y being FinSequence of COMPLEX st len x = len y holds
(x + y) . i = (x . i) + (y . i)

proof end;

definition

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

proof end;

end;

:: deftheorem defines Re COMPLSP2:def 2 :

theorem Th27: :: COMPLSP2:27

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

proof end;

definition

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

proof end;

end;

:: deftheorem defines Im COMPLSP2:def 3 :

definition

end;

:: deftheorem defines |( COMPLSP2:def 4 :

theorem Th28: :: COMPLSP2:28

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
x + (y + z) = (x + y) + z

proof end;

theorem Th29: :: COMPLSP2:29

for x, y being FinSequence of COMPLEX st len x = len y holds
x + y = y + x

proof end;

theorem Th30: :: COMPLSP2:30

for c being complex number
for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x + y) = (c * x) + (c * y)

proof end;

theorem Th31: :: COMPLSP2:31

for x, y being FinSequence of COMPLEX st len x = len y holds
x - y = x + (- y)

proof end;

definition

let i be Nat;
let c be Element of COMPLEX ;
:: original: |->
redefine func i |-> c -> Element of i -tuples_on COMPLEX ;
coherence by FINSEQ_2:132;

end;

theorem Th32: :: COMPLSP2:32

for x, y being FinSequence of COMPLEX st len x = len y & x + y = 0c (len x) holds
( x = - y & y = - x )

proof end;

theorem Th33: :: COMPLSP2:33

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

proof end;

theorem Th34: :: COMPLSP2:34

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

proof end;

theorem Th35: :: COMPLSP2:35

for x, y being FinSequence of COMPLEX st len x = len y holds
- (x + y) = (- x) + (- y)

proof end;

theorem Th36: :: COMPLSP2:36

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
(x - y) - z = x - (y + z)

proof end;

theorem Th37: :: COMPLSP2:37

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
x + (y - z) = (x + y) - z

proof end;

theorem Th38: :: COMPLSP2:38

for x being FinSequence of COMPLEX holds - (- x) = x

proof end;

theorem Th39: :: COMPLSP2:39

for x, y being FinSequence of COMPLEX st len x = len y holds
- (x - y) = (- x) + y

proof end;

theorem Th40: :: COMPLSP2:40

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
x - (y - z) = (x - y) + z

proof end;

theorem Th41: :: COMPLSP2:41

for x being FinSequence of COMPLEX
for c being complex number holds c * (0c (len x)) = 0c (len x)

proof end;

theorem Th42: :: COMPLSP2:42

for x being FinSequence of COMPLEX
for c being complex number holds - (c * x) = c * (- x)

proof end;

theorem Th43: :: COMPLSP2:43

for c being complex number
for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x - y) = (c * x) - (c * y)

proof end;

theorem :: COMPLSP2:44

for x1, y1 being Element of COMPLEX
for x2, y2 being Real st x1 = x2 & y1 = y2 holds
addcomplex . x1,y1 = addreal . x2,y2

proof end;

theorem Th45: :: COMPLSP2:45

for C being Function of [:COMPLEX ,COMPLEX :], COMPLEX
for G being Function of [:REAL ,REAL :], REAL
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Nat st i in dom x1 holds
C . (x1 . i),(y1 . i) = G . (x2 . i),(y2 . i) ) holds
C .: x1,y1 = G .: x2,y2

proof end;

Lm2: 0 = 0c
;

definition

let z be FinSequence of REAL ;
let i be set ;
:: original: .
redefine func z . i -> Element of REAL ;
coherence

proof end;

end;

theorem Th46: :: COMPLSP2:46

for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
addcomplex .: x1,y1 = addreal .: x2,y2

proof end;

theorem Th47: :: COMPLSP2:47

for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
x1 + y1 = x2 + y2

proof end;

theorem Th48: :: COMPLSP2:48

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

proof end;

theorem Th49: :: COMPLSP2:49

for x, y being FinSequence of COMPLEX st len x = len y holds
( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )

proof end;

theorem Th50: :: COMPLSP2:50

for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
diffcomplex .: x1,y1 = diffreal .: x2,y2

proof end;

theorem Th51: :: COMPLSP2:51

for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
x1 - y1 = x2 - y2

proof end;

theorem Th52: :: COMPLSP2:52

for x, y being FinSequence of COMPLEX st len x = len y holds
( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )

proof end;

theorem Th53: :: COMPLSP2:53

for z being FinSequence of COMPLEX
for a, b being complex number holds a * (b * z) = (a * b) * z

proof end;

Lm3: for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)

proof end;

theorem Th54: :: COMPLSP2:54

for x being FinSequence of COMPLEX
for c being complex number holds (- c) * x = - (c * x)

proof end;

theorem Th55: :: COMPLSP2:55

for h being Function of COMPLEX , COMPLEX
for g being Function of REAL , REAL
for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Nat st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2

proof end;

theorem Th56: :: COMPLSP2:56

for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds
compcomplex * y1 = compreal * y2

proof end;

theorem Th57: :: COMPLSP2:57

for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds
- y1 = - y2

proof end;

theorem Th58: :: COMPLSP2:58

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

proof end;

theorem Th59: :: COMPLSP2:59

for x, y being FinSequence of COMPLEX st len x = len y holds
|(( * x),y)| = * |(x,y)|

proof end;

theorem Th60: :: COMPLSP2:60

for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,( * y))| = - ( * |(x,y)|)

proof end;

theorem Th61: :: COMPLSP2:61

for a1 being Element of COMPLEX
for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex ) * y1 = (a2 multreal ) * y2

proof end;

theorem Th62: :: COMPLSP2:62

for a1 being complex number
for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
a1 * y1 = a2 * y2

proof end;

theorem Th63: :: COMPLSP2:63

for z being FinSequence of COMPLEX
for a, b being complex number holds (a + b) * z = (a * z) + (b * z)

proof end;

theorem Th64: :: COMPLSP2:64

for z being FinSequence of COMPLEX
for a, b being complex number holds (a - b) * z = (a * z) - (b * z)

proof end;

theorem Th65: :: COMPLSP2:65

for a being Element of COMPLEX
for x being FinSequence of COMPLEX holds
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )

proof end;

theorem Th66: :: COMPLSP2:66

for x1, x2, y being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y holds
|((x1 + x2),y)| = |(x1,y)| + |(x2,y)|

proof end;

theorem Th67: :: COMPLSP2:67

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|((- x1),x2)| = - |(x1,x2)|

proof end;

theorem Th68: :: COMPLSP2:68

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|(x1,(- x2))| = - |(x1,x2)|

proof end;

theorem :: COMPLSP2:69

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|((- x1),(- x2))| = |(x1,x2)|

proof end;

theorem Th70: :: COMPLSP2:70

for x1, x2, x3 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len x3 holds
|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|

proof end;

theorem Th71: :: COMPLSP2:71

for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds
|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|

proof end;

theorem Th72: :: COMPLSP2:72

for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds
|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|

proof end;

theorem Th73: :: COMPLSP2:73

for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th74: :: COMPLSP2:74

for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th75: :: COMPLSP2:75

for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,y)| = |(y,x)| *'

proof end;

theorem :: COMPLSP2:76

for x, y being FinSequence of COMPLEX st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|

proof end;

theorem :: COMPLSP2:77

for x, y being FinSequence of COMPLEX st len x = len y holds
|((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|

proof end;

theorem Th78: :: COMPLSP2:78

for a being Element of COMPLEX
for x, y being FinSequence of COMPLEX st len x = len y holds
|((a * x),y)| = a * |(x,y)|

proof end;

theorem Th79: :: COMPLSP2:79

for a being Element of COMPLEX
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(a * y))| = (a *' ) * |(x,y)|

proof end;

theorem :: COMPLSP2:80

for a, b being Element of COMPLEX
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)

proof end;

theorem :: COMPLSP2:81

for a, b being Element of COMPLEX
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(x,((a * y) + (b * z)))| = ((a *' ) * |(x,y)|) + ((b *' ) * |(x,z)|)

proof end;