:: The Inner Product and Conjugate of Matrix of Complex Numbers :: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura :: :: Received October 10, 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 NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, MATRIX_1, ARYTM_3, FINSEQ_1, TREES_1, RELAT_1, CARD_1, XXREAL_0, ZFMISC_1, XCMPLX_0, COMPLFLD, MATRIX_5, ARYTM_1, COMPLEX1, QC_LANG1, FUNCT_1, RVSUM_1, BINOP_2, TARSKI, XBOOLE_0, CARD_3, INCSP_1, FUNCOP_1, SETWISEO, ORDINAL4, PARTFUN1, MATRIXC1, FUNCT_7; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1, RELSET_1, FUNCT_2, ZFMISC_1, NAT_D, PARTFUN1, BINOP_1, FUNCOP_1, NAT_1, FINSEQ_1, FINSEQOP, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2, MATRIX_5, MATRIX_0, MATRIX_3, MATRIX_4, RLVECT_1, COMPLSP2, SETWOP_2, COMPLFLD, STRUCT_0, GROUP_1; constructors SETWISEO, FINSOP_1, MATRIX_3, MATRIX_4, MATRIX_5, SEQ_4, BINOP_2, BINOP_1, RVSUM_1, NAT_D, RELSET_1, COMPLSP2, PRE_POLY, REAL_1; registrations XBOOLE_0, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, BINOP_2, FINSEQ_2, COMPLFLD, MATRIX_0, VALUED_0, RELSET_1, XREAL_0, ORDINAL1, MEMBERED; requirements NUMERALS, SUBSET, REAL, ARITHM; begin reserve i,j,n,k for Nat, a for Element of COMPLEX, R1,R2 for Element of i-tuples_on COMPLEX; definition let M be Matrix of COMPLEX; func M*' -> Matrix of COMPLEX means :: MATRIXC1:def 1 len it=len M & width it=width M & for i,j being Nat st [i,j] in Indices M holds it*(i,j) = (M*(i,j))*'; involutiveness; end; theorem :: MATRIXC1:1 for M be tabular FinSequence holds [i,j] in Indices M iff 1<= i & i<=len M & 1<=j & j<=width M; ::$CT theorem :: MATRIXC1:3 for a being Complex,M being Matrix of COMPLEX holds len (a *M)=len M & width (a*M)=width M; theorem :: MATRIXC1:4 for i,j being Nat,a being Complex,M being Matrix of COMPLEX st [i,j] in Indices M holds (a*M)*(i,j) = a*(M*(i,j)); theorem :: MATRIXC1:5 for a being Complex,M being Matrix of COMPLEX holds (a*M) *' = a*'*(M*'); theorem :: MATRIXC1:6 for M1,M2 being Matrix of COMPLEX holds len (M1+M2)=len M1 & width (M1+M2)=width M1; theorem :: MATRIXC1:7 for i,j being Nat,M1,M2 being Matrix of COMPLEX st [i,j] in Indices M1 holds (M1+M2)*(i,j) = M1*(i,j) + M2*(i,j); theorem :: MATRIXC1:8 for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2 holds (M1 + M2)*' = M1*' + M2*'; theorem :: MATRIXC1:9 for M being Matrix of COMPLEX holds len (-M)=len M & width (-M)= width M; theorem :: MATRIXC1:10 for i,j being Nat,M being Matrix of COMPLEX st [i,j] in Indices M holds (-M)*(i,j)= -(M*(i,j)); theorem :: MATRIXC1:11 for M being Matrix of COMPLEX holds (-1)*M = -M; theorem :: MATRIXC1:12 for M being Matrix of COMPLEX holds (-M)*' = -(M*'); theorem :: MATRIXC1:13 for M1,M2 being Matrix of COMPLEX holds len (M1-M2)=len M1 & width (M1-M2)=width M1; theorem :: MATRIXC1:14 for i,j being Nat,M1,M2 be Matrix of COMPLEX st len M1=len M2 & width M1=width M2 & [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i ,j)); theorem :: MATRIXC1:15 for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2 holds (M1 - M2)*' = M1*' - M2*'; definition let M be Matrix of COMPLEX; func M@" -> Matrix of COMPLEX equals :: MATRIXC1:def 2 (M@)*'; end; definition let x be FinSequence of COMPLEX; assume len x > 0; func FinSeq2Matrix x -> Matrix of COMPLEX means :: MATRIXC1:def 3 len it = len x & width it = 1 & for j st j in Seg len x holds it.j =<*x.j*>; end; definition let M be Matrix of COMPLEX; func Matrix2FinSeq M -> FinSequence of COMPLEX equals :: MATRIXC1:def 4 Col(M,1); end; definition let F1,F2 be FinSequence of COMPLEX; func mlt(F1,F2) -> FinSequence of COMPLEX equals :: MATRIXC1:def 5 multcomplex.:(F1,F2); commutativity; end; definition let M be Matrix of COMPLEX; let F be FinSequence of COMPLEX; func M*F -> FinSequence of COMPLEX means :: MATRIXC1:def 6 len it = len M & for i st i in Seg len M holds it.i=Sum mlt(Line(M,i),F); end; theorem :: MATRIXC1:16 a*mlt(R1,R2) = mlt(a*R1,R2); definition let M be Matrix of COMPLEX; let a be Complex; func M*a -> Matrix of COMPLEX equals :: MATRIXC1:def 7 a*M; end; theorem :: MATRIXC1:17 for a being Element of COMPLEX,M being Matrix of COMPLEX holds (M*a)*' = a*'*(M*'); theorem :: MATRIXC1:18 for F1,F2 being FinSequence of COMPLEX,i being Nat holds i in dom mlt(F1,F2) implies mlt(F1,F2).i = F1.i * F2.i; definition let i be Element of NAT, R1,R2 be Element of i-tuples_on COMPLEX; redefine func mlt(R1,R2) -> Element of i-tuples_on COMPLEX; end; theorem :: MATRIXC1:19 mlt(R1,R2).j = R1.j * R2.j; ::$CT theorem :: MATRIXC1:21 for F being FinSequence of COMPLEX ex G being sequence of COMPLEX st for n being Nat st 1<= n & n<=len F holds G.n=F.n; theorem :: MATRIXC1:22 for F being FinSequence of COMPLEX st len (F*') >= 1 holds addcomplex $$ (F*') = (addcomplex $$ F)*'; theorem :: MATRIXC1:23 for F being FinSequence of COMPLEX st len F >= 1 holds Sum(F*') = (Sum F)*'; theorem :: MATRIXC1:24 for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x ,(y*')))*' = mlt(y,(x*')); theorem :: MATRIXC1:25 for x,y being FinSequence of COMPLEX,a being Element of COMPLEX st len x=len y holds (mlt(x,a*y)) = a*mlt(x,y); theorem :: MATRIXC1:26 for x,y being FinSequence of COMPLEX,a being Element of COMPLEX st len x=len y holds mlt(a*x,y) = a*mlt(x,y); theorem :: MATRIXC1:27 for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x ,y))*' = mlt(x*',y*'); theorem :: MATRIXC1:28 for F being FinSequence of COMPLEX,a being Element of COMPLEX holds Sum(a*F) = a*(Sum F); definition let x be FinSequence of REAL; func FR2FC(x) -> FinSequence of COMPLEX equals :: MATRIXC1:def 8 x; end; theorem :: MATRIXC1:29 for R being FinSequence of REAL, F being FinSequence of COMPLEX st R = F & len R >= 1 holds addreal $$ R = addcomplex $$ F; theorem :: MATRIXC1:30 for x being FinSequence of REAL, y being FinSequence of COMPLEX st x=y & len x >=1 holds Sum x = Sum y; theorem :: MATRIXC1:31 for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds Sum(F1 - F2) = Sum F1 - Sum F2; theorem :: MATRIXC1:32 for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z holds mlt((x-y),z) = mlt(x,z)-mlt(y,z); theorem :: MATRIXC1:33 for x,y,z being FinSequence of COMPLEX st len x=len y & len y= len z holds mlt(x,y-z) = mlt(x,y)-mlt(x,z); theorem :: MATRIXC1:34 for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z holds mlt(x,y+z) = mlt(x,y)+mlt(x,z); theorem :: MATRIXC1:35 for x,y,z being FinSequence of COMPLEX st len x=len y & len y= len z holds mlt((x+y),z) = mlt(x,z)+mlt(y,z); theorem :: MATRIXC1:36 for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds Sum(F1 + F2) = Sum F1 + Sum F2; theorem :: MATRIXC1:37 for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds multcomplex.:(x1 ,y1) = multreal.:(x2,y2); theorem :: MATRIXC1:38 for x,y being FinSequence of REAL st len x=len y holds FR2FC mlt(x,y)= mlt(FR2FC x,FR2FC y); theorem :: MATRIXC1:39 for x,y being FinSequence of COMPLEX st len x=len y holds |( x,y )| = Sum mlt(x,(y*')); theorem :: MATRIXC1:40 for i,j being Nat,M1,M2 being Matrix of COMPLEX st width M1=width M2 & j in Seg len M1 holds Line(M1+M2,j)=Line(M1,j)+Line(M2,j); theorem :: MATRIXC1:41 for M being Matrix of COMPLEX st i in Seg len M holds Line(M,i)= (Line(M*',i))*'; theorem :: MATRIXC1:42 for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st len F=width M holds mlt(F,(Line((M*'),i))*') = mlt(Line((M*'),i),(F*'))*'; theorem :: MATRIXC1:43 for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st len F = width M & len F >= 1 holds (M*F)*'=(M*')*(F*'); theorem :: MATRIXC1:44 for F1,F2,F3 being FinSequence of COMPLEX st len F1 = len F2 & len F2 = len F3 holds mlt(F1,mlt(F2,F3)) = mlt(mlt(F1,F2),F3); theorem :: MATRIXC1:45 for F being FinSequence of COMPLEX holds Sum -F = -(Sum F); theorem :: MATRIXC1:46 for F1,F2 being FinSequence of COMPLEX holds Sum(F1^F2) = Sum F1 + Sum F2; definition let M be Matrix of COMPLEX; func LineSum M -> FinSequence of COMPLEX means :: MATRIXC1:def 9 len it=len M & for i being Nat st i in Seg len M holds it.i=Sum Line(M,i); end; definition let M be Matrix of COMPLEX; func ColSum M -> FinSequence of COMPLEX means :: MATRIXC1:def 10 len it=width M & for j being Nat st j in Seg width M holds it.j=Sum (Col(M,j)); end; theorem :: MATRIXC1:47 for F being FinSequence of COMPLEX holds len F = 1 implies Sum F = F.1; theorem :: MATRIXC1:48 for f,g being FinSequence of COMPLEX,n being Nat st len f = n + 1 & g = f|n holds Sum f = Sum g + f/.(len f); theorem :: MATRIXC1:49 for M being Matrix of COMPLEX st len M > 0 holds Sum LineSum M = Sum ColSum M ; definition let M be Matrix of COMPLEX; func SumAll M -> Element of COMPLEX equals :: MATRIXC1:def 11 Sum LineSum M; end; theorem :: MATRIXC1:50 for M being Matrix of COMPLEX holds ColSum M = LineSum(M@); theorem :: MATRIXC1:51 for M being Matrix of COMPLEX st len M > 0 holds SumAll M = SumAll (M@); definition let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX; assume that len x=len M and len y=width M; func QuadraticForm(x,M,y) -> Matrix of COMPLEX means :: MATRIXC1:def 12 len it = len x & width it=len y & for i,j being Nat st [i,j] in Indices M holds it*(i,j)=(x.i) *(M*(i,j))*((y.j)*'); end; theorem :: MATRIXC1:52 for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len x = len M & len y = width M & len y > 0 holds (QuadraticForm(x,M,y))@ = (QuadraticForm(y,M@",x))*'; theorem :: MATRIXC1:53 for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len x=len M & len y =width M holds (QuadraticForm(x,M,y))*'=QuadraticForm(x *',M*',y*'); theorem :: MATRIXC1:54 for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y holds |(x,y)|=(|(y,x)|)*'; theorem :: MATRIXC1:55 for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y holds (|(x,y)|)*'=|(x*',y*')|; theorem :: MATRIXC1:56 for M being Matrix of COMPLEX st width M > 0 holds (M@)*' =(M*')@; theorem :: MATRIXC1:57 for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len x=width M & len y = len M & len x>0 & len y>0 holds |(x,(M@")*y)| = SumAll QuadraticForm(x,M@,y); theorem :: MATRIXC1:58 for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len y=len M & len x =width M & len x>0 & len y>0 holds |(M*x,y)| = SumAll QuadraticForm(x,M@,y); theorem :: MATRIXC1:59 for x,y being FinSequence of COMPLEX, M being Matrix of COMPLEX st len x=width M & len y =len M & width M>0 & len M>0 holds |(M*x,y)| = |(x,(M @")*y)|; theorem :: MATRIXC1:60 for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len x=len M & len y =width M & width M>0 & len M>0 holds |(x,M*y)| = |((M@")*x,y)|;