:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, ARYTM_3, NAT_1, XXREAL_0, FUNCT_1, RELAT_1, TARSKI, BINOP_2, FUNCOP_1, ARYTM_1, XCMPLX_0, CARD_1, COMPLEX1, RVSUM_1, REAL_1, ZFMISC_1, VALUED_0, VALUED_1; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2, MATRIX_5, XXREAL_0, COMSEQ_2; constructors SETWISEO, REAL_1, BINOP_2, FINSEQOP, SEQ_4, MATRIX_5, BINOP_1, RVSUM_1, RELSET_1, COMSEQ_2; registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, VALUED_1, XREAL_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve i,j for Element of NAT, x,y,z for FinSequence of COMPLEX, c for Element of COMPLEX, R,R1,R2 for Element of i-tuples_on COMPLEX; definition let z be FinSequence of COMPLEX; redefine func z*' -> FinSequence of COMPLEX means :: COMPLSP2:def 1 len it = len z & for i being Nat st 1<=i & i<=len z holds it.i = (z.i)*'; end; theorem :: COMPLSP2:1 i in dom (x+y) implies (x+y).i = x.i + y.i; theorem :: COMPLSP2:2 i in dom (x-y) implies (x-y).i = x.i - y.i; definition let i,R1,R2; redefine func R1 - R2 -> Element of i-tuples_on COMPLEX; end; definition let i,R1,R2; redefine func R1 + R2 -> Element of i-tuples_on COMPLEX; end; definition let i, R; let r be Complex; redefine func r*R -> Element of i-tuples_on COMPLEX; end; theorem :: COMPLSP2:3 for a being Complex, x being complex-valued FinSequence holds len (a(#)x) = len x; theorem :: COMPLSP2:4 for x being complex-valued FinSequence holds dom x = dom -x; theorem :: COMPLSP2:5 for x being complex-valued FinSequence holds len (-x)=len x; theorem :: COMPLSP2:6 for x1,x2 being complex-valued FinSequence st len x1=len x2 holds len (x1+x2)=len x1; theorem :: COMPLSP2:7 for x1,x2 being complex-valued FinSequence st len x1=len x2 holds len (x1-x2)=len x1; theorem :: COMPLSP2:8 for f being complex-valued FinSequence holds f is Element of COMPLEX len f; ::$CT 4 theorem :: COMPLSP2:13 for x being FinSequence of COMPLEX holds (-x).i = -x.i; definition let i,R; redefine func -R -> Element of i-tuples_on COMPLEX; end; theorem :: COMPLSP2:14 c = R.j implies (-R).j = -c; theorem :: COMPLSP2:15 for a being Complex holds dom(a*x) = dom x; theorem :: COMPLSP2:16 for i being Nat, a being Complex holds (a*x).i = a*(x.i); theorem :: COMPLSP2:17 for a being Complex holds (a*x)*' = a*'*(x*'); theorem :: COMPLSP2:18 (R1+R2).j = R1.j + R2.j; theorem :: COMPLSP2:19 for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds (x1 + x2)*' = x1*' + x2*'; theorem :: COMPLSP2:20 (R1-R2).j = R1.j - R2.j; theorem :: COMPLSP2:21 for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds (x1 - x2)*' = x1*' - x2*'; theorem :: COMPLSP2:22 for z being FinSequence of COMPLEX holds (z*')*' = z; theorem :: COMPLSP2:23 for z being FinSequence of COMPLEX holds (-z)*' = -(z*'); theorem :: COMPLSP2:24 for z being Complex holds z+z*' = 2*(Re z); theorem :: COMPLSP2:25 for x,y being complex-valued FinSequence st len x=len y holds (x-y).i = x.i - y.i; theorem :: COMPLSP2:26 for x,y being complex-valued FinSequence st len x=len y holds (x+y).i = x.i + y.i; definition let z be FinSequence of COMPLEX; func Re z -> FinSequence of REAL equals :: COMPLSP2:def 2 1/2*(z+z*'); end; theorem :: COMPLSP2:27 for z being Complex holds z-z*' = 2*(Im z) * ; definition let z be FinSequence of COMPLEX; func Im z -> FinSequence of REAL equals :: COMPLSP2:def 3 (-1/2*)*(z-z*'); end; 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)|; end; theorem :: 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; ::$CT theorem :: COMPLSP2:30 for c being Complex, x,y being FinSequence of COMPLEX st len x=len y holds c*(x+y) = c*x + c*y; ::$CT theorem :: COMPLSP2:32 for x,y being complex-valued FinSequence st len x=len y & x + y = 0c (len x) holds x = -y & y = -x; theorem :: COMPLSP2:33 for x being complex-valued FinSequence holds x + 0c (len x) = x; theorem :: COMPLSP2:34 for x being complex-valued FinSequence holds x + -x = 0c (len x); theorem :: COMPLSP2:35 for x,y being complex-valued FinSequence st len x=len y holds -(x + y) = -x + -y; theorem :: 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); theorem :: 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; ::$CT theorem :: COMPLSP2:39 for x,y being complex-valued FinSequence st len x=len y holds -(x - y) = -x + y; theorem :: 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; theorem :: COMPLSP2:41 for c being Complex holds c*(0c (len x)) = 0c (len x); theorem :: COMPLSP2:42 for c being Complex holds -c*x = c*(-x); theorem :: COMPLSP2:43 for c being Complex, x,y being FinSequence of COMPLEX st len x=len y holds c*(x-y) = c*x - c*y; 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); reserve C for Function of [:COMPLEX,COMPLEX:],COMPLEX; reserve G for Function of [:REAL,REAL:],REAL; theorem :: COMPLSP2:45 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 st i in dom x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i)) holds C.:(x1,y1)=G.:(x2,y2); 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); ::$CT theorem :: COMPLSP2:48 for x being FinSequence of COMPLEX holds len (Re x)=len x & len (Im x)=len x; theorem :: 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; 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); ::$CT theorem :: 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; theorem :: COMPLSP2:53 for a, b being Complex holds a*(b*z) = (a*b)*z; theorem :: COMPLSP2:54 for c being Complex holds (-c)*x = -(c*x); reserve h for Function of COMPLEX,COMPLEX, g for Function of REAL,REAL; theorem :: COMPLSP2:55 for y1 being FinSequence of COMPLEX for y2 being FinSequence of REAL st len y1=len y2 & (for i st i in dom y1 holds h.(y1.i)=g.(y2.i)) holds h* y1 = g*y2; 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; ::$CT theorem :: COMPLSP2:58 for x being FinSequence of COMPLEX holds Re (*x) = -(Im x) & Im (*x) = Re x; theorem :: COMPLSP2:59 for x,y being FinSequence of COMPLEX st len x=len y holds |(*x,y)| = *(|(x,y)|); theorem :: COMPLSP2:60 for x,y being FinSequence of COMPLEX st len x=len y holds |(x, *y)| = -*(|(x,y)|); theorem :: COMPLSP2:61 for a1 being Element of COMPLEX,y1 being FinSequence of COMPLEX for a2 being Element of REAL,y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1=len y2 holds (a1 multcomplex)*y1 = (a2 multreal)*y2; ::$CT theorem :: COMPLSP2:63 for a, b being Complex holds (a+b)*z = a*z + b*z; theorem :: COMPLSP2:64 for a, b being Complex holds (a-b)*z = a*z - b*z; theorem :: COMPLSP2:65 for a being Element of COMPLEX,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; begin :: The Inner Product and Conjugate of Finite Sequences theorem :: 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)|; theorem :: COMPLSP2:67 for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds |(-x1, x2)| = -|(x1, x2)|; theorem :: COMPLSP2:68 for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds |(x1, -x2)| = -|(x1, x2)|; theorem :: COMPLSP2:69 for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds |(-x1, -x2)| = |(x1, x2)|; theorem :: 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)|; theorem :: 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)|; theorem :: 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)|; theorem :: 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)|; theorem :: 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)|; theorem :: COMPLSP2:75 for x,y being FinSequence of COMPLEX holds |(x,y)| = (|(y,x)|)*'; 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)|; 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)|; theorem :: COMPLSP2:78 for a being Element of COMPLEX, x,y being FinSequence of COMPLEX st len x=len y holds |(a*x,y)| = a*(|(x,y)|); theorem :: COMPLSP2:79 for a being Element of COMPLEX, x,y being FinSequence of COMPLEX st len x=len y holds |(x,a*y)| = (a*')*(|(x,y)|); theorem :: COMPLSP2:80 for a,b being Element of COMPLEX,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)|; theorem :: COMPLSP2:81 for a,b being Element of COMPLEX,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)| ;