:: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: 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,())) * 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 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
proof end;

theorem Th38: :: COMPLSP2:45
for C being Function of ,COMPLEX
for G being Function of ,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
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 () * 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;