:: 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-2012 Association of Mizar Users begin definition let z be FinSequence of COMPLEX ; funcz *' -> 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 ex b1 being FinSequence of COMPLEX st ( len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds b1 . i = (z . i) *' ) ) proofend; uniqueness for b1, b2 being FinSequence of COMPLEX st len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds b1 . i = (z . i) *' ) & len b2 = len z & ( for i being Nat st 1 <= i & i <= len z holds b2 . i = (z . i) *' ) holds b1 = b2 proofend; 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 proofend; 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 funcR1 - R2 -> Element of i -tuples_on COMPLEX; coherence R1 - R2 is Element of i -tuples_on COMPLEX proofend; end; definition let i be Element of NAT ; let R1, R2 be Element of i -tuples_on COMPLEX; :: original:+ redefine funcR1 + R2 -> Element of i -tuples_on COMPLEX; coherence R1 + R2 is Element of i -tuples_on COMPLEX proofend; end; definition let i be Element of NAT ; let R be Element of i -tuples_on COMPLEX; let r be complex number ; :: original:* redefine funcr * R -> Element of i -tuples_on COMPLEX; coherence r * R is Element of i -tuples_on COMPLEX proofend; end; theorem Th3: :: COMPLSP2:3 for a being complex number for x being FinSequence of COMPLEX holds len (a * x) = len x proofend; theorem :: COMPLSP2:4 for x being complex-yielding 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 proofend; Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX proofend; theorem Th6: :: COMPLSP2:6 for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds len (x1 + x2) = len x1 proofend; theorem Th7: :: COMPLSP2:7 for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds len (x1 - x2) = len x1 proofend; theorem :: COMPLSP2:8 for f being complex-valued FinSequence holds f is Element of COMPLEX (len f) proofend; theorem :: COMPLSP2:9 for i being Element of NAT for R1, R2 being Element of i -tuples_on COMPLEX holds R1 - R2 = R1 + (- R2) ; theorem :: COMPLSP2:10 for x, y being complex-valued FinSequence st len x = len y holds x - y = x + (- y) ; theorem :: COMPLSP2:11 for i being Element of NAT for R being Element of i -tuples_on COMPLEX holds (- 1) * R = - R ; theorem :: COMPLSP2:12 for x being FinSequence of COMPLEX holds (- 1) * x = - x ; theorem Th13: :: COMPLSP2:13 for i being Element of NAT for x being FinSequence of COMPLEX holds (- x) . i = - (x . i) proofend; 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 proofend; 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 Th13; theorem Th15: :: COMPLSP2:15 for x being FinSequence of COMPLEX for a being complex number holds dom (a * x) = dom x proofend; theorem Th16: :: COMPLSP2:16 for x being FinSequence of COMPLEX for i being Nat for a being complex number holds (a * x) . i = a * (x . i) proofend; theorem Th17: :: COMPLSP2:17 for x being FinSequence of COMPLEX for a being complex number holds (a * x) *' = (a *') * (x *') proofend; theorem Th18: :: 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) proofend; theorem Th19: :: COMPLSP2:19 for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds (x1 + x2) *' = (x1 *') + (x2 *') proofend; theorem Th20: :: 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) proofend; theorem Th21: :: COMPLSP2:21 for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds (x1 - x2) *' = (x1 *') - (x2 *') proofend; theorem :: COMPLSP2:22 for z being FinSequence of COMPLEX holds (z *') *' = z proofend; theorem :: COMPLSP2:23 for z being FinSequence of COMPLEX holds (- z) *' = - (z *') proofend; theorem Th24: :: COMPLSP2:24 for z being complex number holds z + (z *') = 2 * (Re z) proofend; theorem Th25: :: 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) proofend; theorem Th26: :: 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) proofend; 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 proofend; end; :: deftheorem defines Re COMPLSP2:def_2_:_ for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *')); theorem Th27: :: COMPLSP2:27 for z being complex number holds z - (z *') = (2 * (Im z)) * proofend; definition let z be FinSequence of COMPLEX ; func Im z -> FinSequence of REAL equals :: COMPLSP2:def 3 (- ((1 / 2) * )) * (z - (z *')); coherence (- ((1 / 2) * )) * (z - (z *')) is FinSequence of REAL proofend; end; :: deftheorem defines Im COMPLSP2:def_3_:_ for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * )) * (z - (z *')); definition let x, y be FinSequence of COMPLEX ; func|(x,y)| -> Element of COMPLEX equals :: COMPLSP2:def 4 ((|((Re x),(Re y))| - ( * |((Re x),(Im y))|)) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))|; coherence ((|((Re x),(Re y))| - ( * |((Re x),(Im y))|)) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX ; end; :: deftheorem defines |( COMPLSP2:def_4_:_ for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - ( * |((Re x),(Im y))|)) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))|; theorem Th28: :: 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 proofend; theorem :: COMPLSP2:29 for x, y being complex-valued FinSequence st len x = len y holds x + y = y + x ; 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) proofend; theorem :: COMPLSP2:31 for x, y being complex-valued FinSequence st len x = len y holds x - y = x + (- y) ; theorem Th32: :: COMPLSP2:32 for x, y being complex-valued FinSequence st len x = len y & x + y = 0c (len x) holds ( x = - y & y = - x ) proofend; theorem Th33: :: COMPLSP2:33 for x being complex-valued FinSequence holds x + (0c (len x)) = x proofend; theorem Th34: :: COMPLSP2:34 for x being complex-valued FinSequence holds x + (- x) = 0c (len x) proofend; theorem Th35: :: COMPLSP2:35 for x, y being complex-valued FinSequence st len x = len y holds - (x + y) = (- x) + (- y) proofend; theorem Th36: :: 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) proofend; theorem Th37: :: 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 proofend; theorem :: COMPLSP2:38 canceled; theorem Th39: :: COMPLSP2:39 for x, y being complex-valued FinSequence st len x = len y holds - (x - y) = (- x) + y proofend; theorem Th40: :: 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 proofend; theorem Th41: :: COMPLSP2:41 for x being FinSequence of COMPLEX for c being complex number holds c * (0c (len x)) = 0c (len x) proofend; theorem Th42: :: COMPLSP2:42 for x being FinSequence of COMPLEX for c being complex number holds - (c * x) = c * (- x) proofend; 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) proofend; 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) proofend; 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 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) proofend; 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) proofend; theorem :: 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 ; theorem Th48: :: COMPLSP2:48 for x being FinSequence of COMPLEX holds ( len (Re x) = len x & len (Im x) = len x ) proofend; 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) ) proofend; 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) proofend; theorem :: 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 ; 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) ) proofend; theorem Th53: :: COMPLSP2:53 for z being FinSequence of COMPLEX for a, b being complex number holds a * (b * z) = (a * b) * z proofend; Lm3: for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x) proofend; theorem Th54: :: COMPLSP2:54 for x being FinSequence of COMPLEX for c being complex number holds (- c) * x = - (c * x) proofend; 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 Element of NAT st i in dom y1 holds h . (y1 . i) = g . (y2 . i) ) holds h * y1 = g * y2 proofend; 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 proofend; theorem :: COMPLSP2:57 for y1 being FinSequence of COMPLEX for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds - y1 = - y2 ; theorem Th58: :: COMPLSP2:58 for x being FinSequence of COMPLEX holds ( Re ( * x) = - (Im x) & Im ( * x) = Re x ) proofend; theorem Th59: :: COMPLSP2:59 for x, y being FinSequence of COMPLEX st len x = len y holds |(( * x),y)| = * |(x,y)| proofend; theorem Th60: :: COMPLSP2:60 for x, y being FinSequence of COMPLEX st len x = len y holds |(x,( * y))| = - ( * |(x,y)|) proofend; 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 proofend; theorem :: 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 ; theorem Th63: :: COMPLSP2:63 for z being FinSequence of COMPLEX for a, b being complex number holds (a + b) * z = (a * z) + (b * z) proofend; theorem Th64: :: COMPLSP2:64 for z being FinSequence of COMPLEX for a, b being complex number holds (a - b) * z = (a * z) - (b * z) proofend; 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)) ) proofend; begin 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)| proofend; theorem Th67: :: COMPLSP2:67 for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds |((- x1),x2)| = - |(x1,x2)| proofend; theorem Th68: :: COMPLSP2:68 for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds |(x1,(- x2))| = - |(x1,x2)| proofend; theorem :: COMPLSP2:69 for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds |((- x1),(- x2))| = |(x1,x2)| proofend; 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)| proofend; 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)| proofend; 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)| proofend; 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)| proofend; 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)| proofend; theorem Th75: :: COMPLSP2:75 for x, y being FinSequence of COMPLEX holds |(x,y)| = |(y,x)| *' proofend; 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)| proofend; 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)| proofend; 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)| proofend; 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)| proofend; 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)|) proofend; 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)|) proofend;