:: 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-2012 Association of Mizar Users


begin

definition
let M be Matrix of COMPLEX;
funcM *'  ->  Matrix of COMPLEX means :Def1: :: 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)) *' ) );
existence
 ex b1 being Matrix of COMPLEX st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) )
proofend;
uniqueness
 for b1, b2 being Matrix of COMPLEX st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = (M * (i,j)) *' ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being Matrix of COMPLEX st len b1 = len b2 & width b1 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b1 * (i,j) = (b2 * (i,j)) *' ) holds
( len b2 = len b1 & width b2 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b2 * (i,j) = (b1 * (i,j)) *' ) )
proofend;
end;

:: deftheorem Def1 defines *' MATRIXC1:def_1_:_
 for M, b2 being Matrix of COMPLEX holds
( b2 = M *' iff ( len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = (M * (i,j)) *' ) ) );

theorem Th1: :: MATRIXC1:1
for i, j being Nat
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( 1 <= i &amp; i <= len M &amp; 1 <= j &amp; j <= width M ) )
proofend;

theorem :: MATRIXC1:2
canceled;

theorem Th3: :: MATRIXC1:3
for a being complex number
for M being Matrix of COMPLEX holds
( len (a * M) = len M &amp; width (a * M) = width M )
proofend;

theorem Th4: :: MATRIXC1:4
for i, j being Nat
for a being complex number
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
proofend;

theorem Th5: :: MATRIXC1:5
for a being complex number
for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
proofend;

theorem Th6: :: MATRIXC1:6
for M1, M2 being Matrix of COMPLEX holds
( len (M1 + M2) = len M1 &amp; width (M1 + M2) = width M1 )
proofend;

theorem Th7: :: MATRIXC1:7
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st [i,j] in Indices M1 holds
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j))
proofend;

theorem :: MATRIXC1:8
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 &amp; width M1 = width M2 holds
(M1 + M2) *' = (M1 *') + (M2 *')
proofend;

theorem Th9: :: MATRIXC1:9
for M being Matrix of COMPLEX holds
( len (- M) = len M &amp; width (- M) = width M )
proofend;

theorem Th10: :: MATRIXC1:10
for i, j being Nat
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
proofend;

theorem Th11: :: MATRIXC1:11
for M being Matrix of COMPLEX holds (- 1) * M = - M
proofend;

theorem :: MATRIXC1:12
for M being Matrix of COMPLEX holds (- M) *' = - (M *')
proofend;

theorem Th13: :: MATRIXC1:13
for M1, M2 being Matrix of COMPLEX holds
( len (M1 - M2) = len M1 &amp; width (M1 - M2) = width M1 )
proofend;

theorem Th14: :: MATRIXC1:14
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 &amp; width M1 = width M2 &amp; [i,j] in Indices M1 holds
(M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
proofend;

theorem :: MATRIXC1:15
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 &amp; width M1 = width M2 holds
(M1 - M2) *' = (M1 *') - (M2 *')
proofend;

definition
let M be Matrix of COMPLEX;
funcM @"  ->  Matrix of COMPLEX equals :: MATRIXC1:def 2
(M @) *' ;
coherence
 (M @) *' is Matrix of COMPLEX ;
end;

:: deftheorem  defines @" MATRIXC1:def_2_:_
 for M being Matrix of COMPLEX holds M @" = (M @) *' ;

definition
let x be FinSequence of COMPLEX ;
assume A1: len x > 0 ;
func FinSeq2Matrix x ->  Matrix of COMPLEX means :: MATRIXC1:def 3
( len it = len x &amp; width it = 1 &amp; ( for j being Nat st j in Seg (len x) holds
it . j = <*(x . j)*> ) );
existence
 ex b1 being Matrix of COMPLEX st
( len b1 = len x &amp; width b1 = 1 &amp; ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) )
proofend;
uniqueness
 for b1, b2 being Matrix of COMPLEX st len b1 = len x &amp; width b1 = 1 &amp; ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) &amp; len b2 = len x &amp; width b2 = 1 &amp; ( for j being Nat st j in Seg (len x) holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines FinSeq2Matrix MATRIXC1:def_3_:_
 for x being FinSequence of COMPLEX st len x > 0 holds
for b2 being Matrix of COMPLEX holds
( b2 = FinSeq2Matrix x iff ( len b2 = len x &amp; width b2 = 1 &amp; ( for j being Nat st j in Seg (len x) holds
b2 . j = <*(x . j)*> ) ) );

definition
let M be Matrix of COMPLEX;
func Matrix2FinSeq M ->  FinSequence of COMPLEX  equals :: MATRIXC1:def 4
 Col (M,1);
coherence
 Col (M,1) is FinSequence of COMPLEX ;
end;

:: deftheorem  defines Matrix2FinSeq MATRIXC1:def_4_:_
 for M being Matrix of COMPLEX holds Matrix2FinSeq M = Col (M,1);

definition
let F1, F2 be FinSequence of COMPLEX ;
func mlt (F1,F2) ->  FinSequence of COMPLEX  equals :: MATRIXC1:def 5
multcomplex .: (F1,F2);
coherence
 multcomplex .: (F1,F2) is FinSequence of COMPLEX ;
commutativity
 for b1, F1, F2 being FinSequence of COMPLEX st b1 = multcomplex .: (F1,F2) holds
b1 = multcomplex .: (F2,F1)
proofend;
end;

:: deftheorem  defines mlt MATRIXC1:def_5_:_
 for F1, F2 being FinSequence of COMPLEX holds mlt (F1,F2) = multcomplex .: (F1,F2);

definition
let M be Matrix of COMPLEX;
let F be FinSequence of COMPLEX ;
funcM * F ->  FinSequence of COMPLEX  means :Def6: :: MATRIXC1:def 6
( len it = len M &amp; ( for i being Nat st i in Seg (len M) holds
it . i = Sum (mlt ((Line (M,i)),F)) ) );
existence
 ex b1 being FinSequence of COMPLEX st
( len b1 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of COMPLEX st len b1 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) &amp; len b2 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (mlt ((Line (M,i)),F)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines * MATRIXC1:def_6_:_
 for M being Matrix of COMPLEX
for F, b3 being FinSequence of COMPLEX holds
( b3 = M * F iff ( len b3 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b3 . i = Sum (mlt ((Line (M,i)),F)) ) ) );

Lm1:  for a being Element of COMPLEX
for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] (a,(id COMPLEX))) * F
proofend;

theorem Th16: :: MATRIXC1:16
for i being Nat
for a being Element of COMPLEX
for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
proofend;

definition
let M be Matrix of COMPLEX;
let a be complex number ;
funcM * a ->  Matrix of COMPLEX equals :: MATRIXC1:def 7
a * M;
coherence
 a * M is Matrix of COMPLEX ;
end;

:: deftheorem  defines * MATRIXC1:def_7_:_
 for M being Matrix of COMPLEX
for a being complex number holds M * a = a * M;

theorem :: MATRIXC1:17
for a being Element of COMPLEX
for M being Matrix of COMPLEX holds (M * a) *' = (a *') * (M *') by Th5;

theorem Th18: :: MATRIXC1:18
for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (mlt (F1,F2)) holds
(mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
proofend;

definition
let i be Element of NAT ;
let R1, R2 be Element of i -tuples_on COMPLEX;
:: original:mlt
redefine func mlt (R1,R2) ->  Element of i -tuples_on COMPLEX;
coherence
 mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem Th19: :: MATRIXC1:19
for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
proofend;

theorem Th20: :: MATRIXC1:20
for a, b being Element of COMPLEX holds (addcomplex . (a,(b *'))) *' = addcomplex . ((a *'),b)
proofend;

theorem Th21: :: MATRIXC1:21
for F being FinSequence of COMPLEX ex G being Function of NAT,COMPLEX st
for n being Nat st 1 <= n &amp; n <= len F holds
G . n = F . n
proofend;

theorem Th22: :: MATRIXC1:22
for F being FinSequence of COMPLEX st len (F *') >= 1 holds
addcomplex $$ (F *') = (addcomplex $$ F) *'
proofend;

theorem Th23: :: MATRIXC1:23
for F being FinSequence of COMPLEX st len F >= 1 holds
Sum (F *') = (Sum F) *'
proofend;

theorem Th24: :: MATRIXC1:24
for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt (x,(y *'))) *' = mlt (y,(x *'))
proofend;

theorem Th25: :: MATRIXC1:25
for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt (x,(a * y)) = a * (mlt (x,y))
proofend;

theorem Th26: :: MATRIXC1:26
for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt ((a * x),y) = a * (mlt (x,y))
proofend;

theorem Th27: :: MATRIXC1:27
for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt (x,y)) *' = mlt ((x *'),(y *'))
proofend;

Lm2:  for a, b being Element of COMPLEX holds (multcomplex [;] (a,(id COMPLEX))) . b = a * b
proofend;

theorem Th28: :: MATRIXC1:28
for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)
proofend;

definition
let x be FinSequence of REAL ;
func FR2FC x ->  FinSequence of COMPLEX  equals :: MATRIXC1:def 8
x;
coherence
 x is FinSequence of COMPLEX
proofend;
end;

:: deftheorem  defines FR2FC MATRIXC1:def_8_:_
 for x being FinSequence of REAL holds FR2FC x = x;

theorem :: MATRIXC1:29
for R being FinSequence of REAL
for F being FinSequence of COMPLEX st R = F &amp; len R >= 1 holds
addreal $$ R = addcomplex $$ F
proofend;

theorem :: MATRIXC1:30
for x being FinSequence of REAL
for y being FinSequence of COMPLEX st x = y &amp; len x >= 1 holds
Sum x = Sum y ;

theorem Th31: :: MATRIXC1:31
for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 - F2) = (Sum F1) - (Sum F2)
proofend;

theorem :: MATRIXC1:32
for x, y, z being FinSequence of COMPLEX st len x = len y &amp; len y = len z holds
mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z))
proofend;

theorem Th33: :: MATRIXC1:33
for x, y, z being FinSequence of COMPLEX st len x = len y &amp; len y = len z holds
mlt (x,(y - z)) = (mlt (x,y)) - (mlt (x,z))
proofend;

theorem :: MATRIXC1:34
for x, y, z being FinSequence of COMPLEX st len x = len y &amp; len y = len z holds
mlt (x,(y + z)) = (mlt (x,y)) + (mlt (x,z))
proofend;

theorem Th35: :: MATRIXC1:35
for x, y, z being FinSequence of COMPLEX st len x = len y &amp; len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
proofend;

theorem Th36: :: MATRIXC1:36
for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 + F2) = (Sum F1) + (Sum F2)
proofend;

theorem Th37: :: MATRIXC1:37
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 &amp; y1 = y2 &amp; len x1 = len y2 holds
multcomplex .: (x1,y1) = multreal .: (x2,y2)
proofend;

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)) by Th37;

theorem Th39: :: MATRIXC1:39
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,y)| = Sum (mlt (x,(y *')))
proofend;

theorem :: MATRIXC1:40
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st width M1 = width M2 &amp; j in Seg (len M1) holds
Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
proofend;

theorem Th41: :: MATRIXC1:41
for i being Nat
for M being Matrix of COMPLEX st i in Seg (len M) holds
Line (M,i) = (Line ((M *'),i)) *'
proofend;

theorem Th42: :: MATRIXC1:42
for i being Nat
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'
proofend;

theorem Th43: :: MATRIXC1:43
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M &amp; len F >= 1 holds
(M * F) *' = (M *') * (F *')
proofend;

theorem :: MATRIXC1:44
for F1, F2, F3 being FinSequence of COMPLEX st len F1 = len F2 &amp; len F2 = len F3 holds
mlt (F1,(mlt (F2,F3))) = mlt ((mlt (F1,F2)),F3)
proofend;

theorem :: MATRIXC1:45
for F being FinSequence of COMPLEX holds Sum (- F) = - (Sum F)
proofend;

theorem Th46: :: MATRIXC1:46
for F1, F2 being FinSequence of COMPLEX holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
proofend;

definition
let M be Matrix of COMPLEX;
func LineSum M ->  FinSequence of COMPLEX  means :Def9: :: MATRIXC1:def 9
( len it = len M &amp; ( for i being Nat st i in Seg (len M) holds
it . i = Sum (Line (M,i)) ) );
existence
 ex b1 being FinSequence of COMPLEX st
( len b1 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of COMPLEX st len b1 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) &amp; len b2 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (Line (M,i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines LineSum MATRIXC1:def_9_:_
 for M being Matrix of COMPLEX
for b2 being FinSequence of COMPLEX holds
( b2 = LineSum M iff ( len b2 = len M &amp; ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (Line (M,i)) ) ) );

definition
let M be Matrix of COMPLEX;
func ColSum M ->  FinSequence of COMPLEX  means :Def10: :: MATRIXC1:def 10
( len it = width M &amp; ( for j being Nat st j in Seg (width M) holds
it . j = Sum (Col (M,j)) ) );
existence
 ex b1 being FinSequence of COMPLEX st
( len b1 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of COMPLEX st len b1 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) &amp; len b2 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines ColSum MATRIXC1:def_10_:_
 for M being Matrix of COMPLEX
for b2 being FinSequence of COMPLEX holds
( b2 = ColSum M iff ( len b2 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) ) );

theorem Th47: :: MATRIXC1:47
for F being FinSequence of COMPLEX st len F = 1 holds
Sum F = F . 1
proofend;

theorem Th48: :: MATRIXC1:48
for f, g being FinSequence of COMPLEX
for n being Nat st len f = n + 1 &amp; g = f | n holds
Sum f = (Sum g) + (f /. (len f))
proofend;

theorem Th49: :: MATRIXC1:49
for M being Matrix of COMPLEX st len M > 0 holds
Sum (LineSum M) = Sum (ColSum M)
proofend;

definition
let M be Matrix of COMPLEX;
func SumAll M ->  Element of COMPLEX  equals :: MATRIXC1:def 11
 Sum (LineSum M);
coherence
 Sum (LineSum M) is Element of COMPLEX ;
end;

:: deftheorem  defines SumAll MATRIXC1:def_11_:_
 for M being Matrix of COMPLEX holds SumAll M = Sum (LineSum M);

theorem Th50: :: MATRIXC1:50
for M being Matrix of COMPLEX holds ColSum M = LineSum (M @)
proofend;

theorem Th51: :: MATRIXC1:51
for M being Matrix of COMPLEX st len M > 0 holds
SumAll M = SumAll (M @)
proofend;

definition
let x, y be FinSequence of COMPLEX ;
let M be Matrix of COMPLEX;
assume that
A1: len x = len M and
A2: len y = width M ;
func QuadraticForm (x,M,y) ->  Matrix of COMPLEX means :Def12: :: MATRIXC1:def 12
( len it = len x &amp; width it = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) );
existence
 ex b1 being Matrix of COMPLEX st
( len b1 = len x &amp; width b1 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
proofend;
uniqueness
 for b1, b2 being Matrix of COMPLEX st len b1 = len x &amp; width b1 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) &amp; len b2 = len x &amp; width b2 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines QuadraticForm MATRIXC1:def_12_:_
 for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M &amp; len y = width M holds
for b4 being Matrix of COMPLEX holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x &amp; width b4 = len y &amp; ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) ) );

theorem Th52: :: MATRIXC1:52
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M &amp; len y = width M &amp; len y > 0 holds
(QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *'
proofend;

theorem Th53: :: MATRIXC1:53
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M &amp; len y = width M holds
(QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
proofend;

theorem Th54: :: MATRIXC1:54
for x, y being FinSequence of COMPLEX st len x = len y &amp; 0 < len y holds
|(x,y)| = |(y,x)| *'
proofend;

theorem Th55: :: MATRIXC1:55
for x, y being FinSequence of COMPLEX st len x = len y &amp; 0 < len y holds
|(x,y)| *' = |((x *'),(y *'))|
proofend;

theorem :: MATRIXC1:56
for M being Matrix of COMPLEX st width M > 0 holds
(M @) *' = (M *') @
proofend;

theorem Th57: :: MATRIXC1:57
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M &amp; len y = len M &amp; len x > 0 &amp; len y > 0 holds
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
proofend;

theorem Th58: :: MATRIXC1:58
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len y = len M &amp; len x = width M &amp; len x > 0 &amp; len y > 0 holds
|((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))
proofend;

theorem Th59: :: MATRIXC1:59
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M &amp; len y = len M &amp; width M > 0 &amp; len M > 0 holds
|((M * x),y)| = |(x,((M @") * y))|
proofend;

theorem :: MATRIXC1:60
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M &amp; len y = width M &amp; width M > 0 &amp; len M > 0 holds
|(x,(M * y))| = |(((M @") * x),y)|
proofend;