:: The Inner Product and Conjugate of Matrix of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: 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,())) * 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 *') = () *' 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,())) . 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 ((),()) 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 () 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 () 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 () holds
b1 . j = Sum (Col (M,j)) ) & len b2 = width M & ( for j being Nat st j in Seg () 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 () 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 () = Sum ()
proof end;

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

:: deftheorem defines SumAll MATRIXC1:def 11 :
for M being Matrix of COMPLEX holds SumAll M = Sum ();

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