:: 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


definition
let M be Matrix of COMPLEX;
func M *' -> 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)) *' ) )
proof end;
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
proof end;
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)) *' ) )
proof end;
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 & i <= len M & 1 <= j & j <= width M ) )
proof end;

theorem :: MATRIXC1:2
canceled;

::$CT
theorem Th2: :: MATRIXC1:3
for a being Complex
for M being Matrix of COMPLEX holds
( len (a * M) = len M & width (a * M) = width M )
proof end;

theorem Th3: :: MATRIXC1:4
for i, j being Nat
for a being Complex
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
proof end;

theorem Th4: :: MATRIXC1:5
for a being Complex
for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
proof end;

theorem Th5: :: MATRIXC1:6
for M1, M2 being Matrix of COMPLEX holds
( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 )
proof end;

theorem Th6: :: 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))
proof end;

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

theorem Th8: :: MATRIXC1:9
for M being Matrix of COMPLEX holds
( len (- M) = len M & width (- M) = width M )
proof end;

theorem Th9: :: 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))
proof end;

theorem Th10: :: MATRIXC1:11
for M being Matrix of COMPLEX holds (- 1) * M = - M
proof end;

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

theorem Th12: :: MATRIXC1:13
for M1, M2 being Matrix of COMPLEX holds
( len (M1 - M2) = len M1 & width (M1 - M2) = width M1 )
proof end;

theorem Th13: :: MATRIXC1:14
for i, j being Nat
for M1, M2 being 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))
proof end;

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

definition
let M be Matrix of COMPLEX;
func M @" -> 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 & width it = 1 & ( 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 & width b1 = 1 & ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) )
proof end;
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = 1 & ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in Seg (len x) holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proof end;
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 & width b2 = 1 & ( 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)
proof end;
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 ;
func M * F -> FinSequence of COMPLEX means :Def6: :: MATRIXC1:def 6
( len it = len M & ( 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 & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) & len b2 = len M & ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (mlt ((Line (M,i)),F)) ) holds
b1 = b2
proof end;
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 & ( 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
proof end;

theorem Th15: :: 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)
proof end;

definition
let M be Matrix of COMPLEX;
let a be Complex;
func M * 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 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 Th4;

theorem Th17: :: 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)
proof end;

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 Th18: :: 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)
proof end;

theorem :: MATRIXC1:20
canceled;

::$CT
theorem Th19: :: 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
proof end;

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

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

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

theorem Th23: :: 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))
proof end;

theorem Th24: :: 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))
proof end;

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

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

theorem Th26: :: MATRIXC1:28
for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)
proof end;

definition
let x be FinSequence of REAL ;
func FR2FC x -> FinSequence of COMPLEX equals :: MATRIXC1:def 8
x;
coherence
x is FinSequence of COMPLEX
proof end;
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 & len R >= 1 holds
addreal $$ R = addcomplex $$ F
proof end;

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

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

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))
proof end;

theorem Th31: :: 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))
proof end;

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))
proof end;

theorem Th33: :: 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))
proof end;

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

theorem Th35: :: 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)
proof end;

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 Th35;

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

theorem :: MATRIXC1:40
for i, j being Nat
for 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))
proof end;

theorem Th39: :: 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)) *'
proof end;

theorem Th40: :: 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 *'))) *'
proof end;

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

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)
proof end;

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

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

definition
let M be Matrix of COMPLEX;
func LineSum M -> FinSequence of COMPLEX means :Def9: :: MATRIXC1:def 9
( len it = len M & ( 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 & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) & len b2 = len M & ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (Line (M,i)) ) holds
b1 = b2
proof end;
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 & ( 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 & ( 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 & ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) & len b2 = width M & ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) holds
b1 = b2
proof end;
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 & ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) ) );

theorem Th45: :: MATRIXC1:47
for F being FinSequence of COMPLEX st len F = 1 holds
Sum F = F . 1
proof end;

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

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

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 Th48: :: MATRIXC1:50
for M being Matrix of COMPLEX holds ColSum M = LineSum (M @)
proof end;

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

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 & 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) *') ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
proof end;
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len b2 = len x & width b2 = len y & ( 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
proof end;
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 & len y = width M holds
for b4 being Matrix of COMPLEX holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x & width b4 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) ) );

theorem Th50: :: MATRIXC1:52
for x, y being FinSequence of COMPLEX
for 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)) *'
proof end;

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

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

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

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

theorem Th55: :: MATRIXC1:57
for x, y being FinSequence of COMPLEX
for 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))
proof end;

theorem Th56: :: MATRIXC1:58
for x, y being FinSequence of COMPLEX
for 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))
proof end;

theorem Th57: :: MATRIXC1:59
for x, y being FinSequence of COMPLEX
for 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))|
proof end;

theorem :: MATRIXC1:60
for x, y being FinSequence of COMPLEX
for 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)|
proof end;