:: 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 b1 being FinSequence of COMPLEX holds
( b1 = z *' iff ( len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b1 . i = (z . i) *' ) ) )
proof end;
end;

:: deftheorem Def1 defines *' COMPLSP2:def 1 :
for z, b2 being FinSequence of COMPLEX holds
( b2 = z *' iff ( len b2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b2 . 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;