:: 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 b₁ being Matrix of COMPLEX st
( len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = (M * (i,j)) *' ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of COMPLEX st len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = (M * (i,j)) *' ) & len b₂ = len M & width b₂ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (i,j) = (M * (i,j)) *' ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Matrix of COMPLEX st len b₁ = len b₂ & width b₁ = width b₂ & ( for i, j being Nat st [i,j] in Indices b₂ holds
b₁ * (i,j) = (b₂ * (i,j)) *' ) holds
( len b₂ = len b₁ & width b₂ = width b₁ & ( for i, j being Nat st [i,j] in Indices b₁ holds
b₂ * (i,j) = (b₁ * (i,j)) *' ) )

proof end;

end;

:: deftheorem Def1 defines *' MATRIXC1:def 1 :
for M, b₂ being Matrix of COMPLEX holds
( b₂ = M *' iff ( len b₂ = len M & width b₂ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (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 b₁ being Matrix of COMPLEX st
( len b₁ = len x & width b₁ = 1 & ( for j being Nat st j in Seg (len x) holds
b₁ . j = <*(x . j)*> ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of COMPLEX st len b₁ = len x & width b₁ = 1 & ( for j being Nat st j in Seg (len x) holds
b₁ . j = <*(x . j)*> ) & len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in Seg (len x) holds
b₂ . j = <*(x . j)*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines FinSeq2Matrix MATRIXC1:def 3 :
for x being FinSequence of COMPLEX st len x > 0 holds
for b₂ being Matrix of COMPLEX holds
( b₂ = FinSeq2Matrix x iff ( len b₂ = len x & width b₂ = 1 & ( for j being Nat st j in Seg (len x) holds
b₂ . 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 b₁, F1, F2 being FinSequence of COMPLEX st b₁ = multcomplex .: (F1,F2) holds
b₁ = 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 b₁ being FinSequence of COMPLEX st
( len b₁ = len M & ( for i being Nat st i in Seg (len M) holds
b₁ . i = Sum (mlt ((Line (M,i)),F)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len M & ( for i being Nat st i in Seg (len M) holds
b₁ . i = Sum (mlt ((Line (M,i)),F)) ) & len b₂ = len M & ( for i being Nat st i in Seg (len M) holds
b₂ . i = Sum (mlt ((Line (M,i)),F)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines * MATRIXC1:def 6 :
for M being Matrix of COMPLEX
for F, b₃ being FinSequence of COMPLEX holds
( b₃ = M * F iff ( len b₃ = len M & ( for i being Nat st i in Seg (len M) holds
b₃ . 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 b₁ being FinSequence of COMPLEX st
( len b₁ = len M & ( for i being Nat st i in Seg (len M) holds
b₁ . i = Sum (Line (M,i)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of COMPLEX st len b₁ = len M & ( for i being Nat st i in Seg (len M) holds
b₁ . i = Sum (Line (M,i)) ) & len b₂ = len M & ( for i being Nat st i in Seg (len M) holds
b₂ . i = Sum (Line (M,i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines LineSum MATRIXC1:def 9 :
for M being Matrix of COMPLEX
for b₂ being FinSequence of COMPLEX holds
( b₂ = LineSum M iff ( len b₂ = len M & ( for i being Nat st i in Seg (len M) holds
b₂ . 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 b₁ being FinSequence of COMPLEX st
( len b₁ = width M & ( for j being Nat st j in Seg (width M) holds
b₁ . j = Sum (Col (M,j)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of COMPLEX st len b₁ = width M & ( for j being Nat st j in Seg (width M) holds
b₁ . j = Sum (Col (M,j)) ) & len b₂ = width M & ( for j being Nat st j in Seg (width M) holds
b₂ . j = Sum (Col (M,j)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines ColSum MATRIXC1:def 10 :
for M being Matrix of COMPLEX
for b₂ being FinSequence of COMPLEX holds
( b₂ = ColSum M iff ( len b₂ = width M & ( for j being Nat st j in Seg (width M) holds
b₂ . 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 b₁ being Matrix of COMPLEX st
( len b₁ = len x & width b₁ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of COMPLEX st len b₁ = len x & width b₁ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len b₂ = len x & width b₂ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) holds
b₁ = b₂

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 b₄ being Matrix of COMPLEX holds
( b₄ = QuadraticForm (x,M,y) iff ( len b₄ = len x & width b₄ = len y & ( for i, j being Nat st [i,j] in Indices M holds
b₄ * (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;