:: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 25, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

definition

let z be FinSequence of COMPLEX ;

:: original: *'
redefine 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) *' ) );

coherence
z *' is FinSequence of COMPLEX

proof end;

compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = z *' iff ( len b₁ = len z & ( for i being Nat st 1 <= i & i <= len z holds
b₁ . i = (z . i) *' ) ) )

proof end;

end;

:: deftheorem Def1 defines *' COMPLSP2:def 1 :
for z, b₂ being FinSequence of COMPLEX holds
( b₂ = z *' iff ( len b₂ = len z & ( for i being Nat st 1 <= i & i <= len z holds
b₂ . i = (z . i) *' ) ) );

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

proof end;

theorem :: COMPLSP2:1

for i being Element of NAT
for x, y being FinSequence of COMPLEX st i in dom (x + y) holds
(x + y) . i = (x . i) + (y . i) by VALUED_1:def 1;

theorem :: COMPLSP2:2

for i being Element of NAT
for x, y being FinSequence of COMPLEX st i in dom (x - y) holds
(x - y) . i = (x . i) - (y . i) by VALUED_1:13;

definition

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

proof end;

end;

definition

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

proof end;

end;

definition

let i be Element of NAT ;
let R be Element of i -tuples_on COMPLEX;
let r be Complex;
:: original: (#)
redefine func r * R -> Element of i -tuples_on COMPLEX;
coherence
r (#) R is Element of i -tuples_on COMPLEX

proof end;

end;

Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX

proof end;

theorem Th3: :: COMPLSP2:3

for a being Complex
for x being complex-valued FinSequence holds len (a (#) x) = len x

proof end;

theorem :: COMPLSP2:4

for x being complex-valued FinSequence holds dom x = dom (- x) by VALUED_1:8;

theorem Th5: :: COMPLSP2:5

for x being complex-valued FinSequence holds len (- x) = len x

proof end;

theorem Th6: :: COMPLSP2:6

for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 + x2) = len x1

proof end;

theorem Th7: :: COMPLSP2:7

for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 - x2) = len x1

proof end;

theorem :: COMPLSP2:8

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

proof end;

theorem :: COMPLSP2:9

canceled;

theorem :: COMPLSP2:10

canceled;

theorem :: COMPLSP2:11

canceled;

theorem :: COMPLSP2:12

canceled;

::$CT 4

theorem Th9: :: COMPLSP2:13

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

proof end;

definition

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

proof end;

end;

theorem :: COMPLSP2:14

for i, j being Element of 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 Th9;

theorem Th11: :: COMPLSP2:15

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

proof end;

theorem Th12: :: COMPLSP2:16

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

proof end;

theorem Th13: :: COMPLSP2:17

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

proof end;

theorem Th14: :: COMPLSP2:18

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

proof end;

theorem Th15: :: COMPLSP2:19

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

proof end;

theorem Th16: :: COMPLSP2:20

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

proof end;

theorem Th17: :: 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 ;

theorem :: COMPLSP2:23

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

proof end;

theorem Th20: :: COMPLSP2:24

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

proof end;

theorem Th21: :: COMPLSP2:25

for i being Element of NAT
for x, y being complex-valued FinSequence st len x = len y holds
(x - y) . i = (x . i) - (y . i)

proof end;

theorem Th22: :: COMPLSP2:26

for i being Element of NAT
for x, y being complex-valued FinSequence 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
(1 / 2) * (z + (z *')) is FinSequence of REAL

proof end;

end;

:: deftheorem defines Re COMPLSP2:def 2 :
for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *'));

theorem Th23: :: COMPLSP2:27

for z being Complex holds z - (z *') = (2 * (Im z)) * <i>

proof end;

definition

let z be FinSequence of COMPLEX ;

func Im z -> FinSequence of REAL equals :: COMPLSP2:def 3
(- ((1 / 2) * <i>)) * (z - (z *'));

coherence
(- ((1 / 2) * <i>)) * (z - (z *')) is FinSequence of REAL

proof end;

end;

:: deftheorem defines Im COMPLSP2:def 3 :
for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i>)) * (z - (z *'));

definition

let x, y be FinSequence of COMPLEX ;

func |(x,y)| -> Element of COMPLEX equals :: COMPLSP2:def 4
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

coherence
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX by XCMPLX_0:def 2;

end;

:: deftheorem defines |( COMPLSP2:def 4 :
for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

theorem Th24: :: COMPLSP2:28

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

proof end;

theorem :: COMPLSP2:29

canceled;

::$CT

theorem Th25: :: COMPLSP2:30

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

proof end;

theorem :: COMPLSP2:31

canceled;

::$CT

theorem Th26: :: COMPLSP2:32

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

proof end;

theorem Th27: :: COMPLSP2:33

for x being complex-valued FinSequence holds x + (0c (len x)) = x

proof end;

theorem Th28: :: COMPLSP2:34

for x being complex-valued FinSequence holds x + (- x) = 0c (len x)

proof end;

theorem Th29: :: COMPLSP2:35

for x, y being complex-valued FinSequence st len x = len y holds
- (x + y) = (- x) + (- y)

proof end;

theorem Th30: :: COMPLSP2:36

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

proof end;

theorem Th31: :: COMPLSP2:37

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

proof end;

theorem :: COMPLSP2:38

canceled;

::$CT

theorem Th32: :: COMPLSP2:39

for x, y being complex-valued FinSequence st len x = len y holds
- (x - y) = (- x) + y

proof end;

theorem Th33: :: COMPLSP2:40

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

proof end;

theorem Th34: :: COMPLSP2:41

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

proof end;

theorem Th35: :: COMPLSP2:42

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

proof end;

theorem Th36: :: COMPLSP2:43

for c being Complex
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 Th38: :: 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 Element of 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;

theorem :: 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 :: COMPLSP2:47

canceled;

::$CT

theorem Th40: :: COMPLSP2:48

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

proof end;

theorem Th41: :: 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 :: 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 :: COMPLSP2:51

canceled;

::$CT

theorem Th43: :: 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 Th44: :: COMPLSP2:53

for z being FinSequence of COMPLEX
for a, b being Complex 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 Th45: :: COMPLSP2:54

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

proof end;

theorem Th46: :: 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 Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2

proof end;

theorem :: 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 :: COMPLSP2:57

canceled;

::$CT

theorem Th48: :: COMPLSP2:58

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

proof end;

theorem Th49: :: COMPLSP2:59

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

proof end;

theorem Th50: :: COMPLSP2:60

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

proof end;

theorem :: 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 :: COMPLSP2:62

canceled;

::$CT

theorem Th52: :: COMPLSP2:63

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

proof end;

theorem Th53: :: COMPLSP2:64

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

proof end;

theorem Th54: :: 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 Th55: :: 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 Th56: :: COMPLSP2:67

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

proof end;

theorem Th57: :: 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 Th59: :: 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 Th60: :: 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 Th61: :: 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 Th62: :: 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 Th63: :: 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 Th64: :: COMPLSP2:75

for x, y being FinSequence of COMPLEX 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 Th67: :: 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 Th68: :: 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;