:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received October 10, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

definition

let M be Matrix of COMPLEX;

ex b_{1} being Matrix of COMPLEX st

( len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = (M * (i,j)) *' ) )

for b_{1}, b_{2} being Matrix of COMPLEX st len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = (M * (i,j)) *' ) & len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = (M * (i,j)) *' ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Matrix of COMPLEX st len b_{1} = len b_{2} & width b_{1} = width b_{2} & ( for i, j being Nat st [i,j] in Indices b_{2} holds

b_{1} * (i,j) = (b_{2} * (i,j)) *' ) holds

( len b_{2} = len b_{1} & width b_{2} = width b_{1} & ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{2} * (i,j) = (b_{1} * (i,j)) *' ) )

end;
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 ( 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)) *' ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

( len b

b

proof end;

:: deftheorem Def1 defines *' MATRIXC1:def 1 :

for M, b_{2} being Matrix of COMPLEX holds

( b_{2} = M *' iff ( len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = (M * (i,j)) *' ) ) );

for M, b

( b

b

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

for M being tabular FinSequence holds

( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )

proof end;

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

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

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

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 *')

(M1 + M2) *' = (M1 *') + (M2 *')

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

for M being Matrix of COMPLEX st [i,j] in Indices M holds

(- M) * (i,j) = - (M * (i,j))

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

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 *')

(M1 - M2) *' = (M1 *') - (M2 *')

proof end;

definition

let x be FinSequence of COMPLEX ;

assume A1: len x > 0 ;

ex b_{1} being Matrix of COMPLEX st

( len b_{1} = len x & width b_{1} = 1 & ( for j being Nat st j in Seg (len x) holds

b_{1} . j = <*(x . j)*> ) )

for b_{1}, b_{2} being Matrix of COMPLEX st len b_{1} = len x & width b_{1} = 1 & ( for j being Nat st j in Seg (len x) holds

b_{1} . j = <*(x . j)*> ) & len b_{2} = len x & width b_{2} = 1 & ( for j being Nat st j in Seg (len x) holds

b_{2} . j = <*(x . j)*> ) holds

b_{1} = b_{2}

end;
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 ( len it = len x & width it = 1 & ( for j being Nat st j in Seg (len x) holds

it . j = <*(x . j)*> ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines FinSeq2Matrix MATRIXC1:def 3 :

for x being FinSequence of COMPLEX st len x > 0 holds

for b_{2} being Matrix of COMPLEX holds

( b_{2} = FinSeq2Matrix x iff ( len b_{2} = len x & width b_{2} = 1 & ( for j being Nat st j in Seg (len x) holds

b_{2} . j = <*(x . j)*> ) ) );

for x being FinSequence of COMPLEX st len x > 0 holds

for b

( b

b

:: deftheorem defines Matrix2FinSeq MATRIXC1:def 4 :

for M being Matrix of COMPLEX holds Matrix2FinSeq M = Col (M,1);

for M being Matrix of COMPLEX holds Matrix2FinSeq M = Col (M,1);

definition

let F1, F2 be FinSequence of COMPLEX ;

coherence

multcomplex .: (F1,F2) is FinSequence of COMPLEX ;

commutativity

for b_{1}, F1, F2 being FinSequence of COMPLEX st b_{1} = multcomplex .: (F1,F2) holds

b_{1} = multcomplex .: (F2,F1)

end;
coherence

multcomplex .: (F1,F2) is FinSequence of COMPLEX ;

commutativity

for b

b

proof end;

:: deftheorem defines mlt MATRIXC1:def 5 :

for F1, F2 being FinSequence of COMPLEX holds mlt (F1,F2) = multcomplex .: (F1,F2);

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 ;

ex b_{1} being FinSequence of COMPLEX st

( len b_{1} = len M & ( for i being Nat st i in Seg (len M) holds

b_{1} . i = Sum (mlt ((Line (M,i)),F)) ) )

for b_{1}, b_{2} being FinSequence of COMPLEX st len b_{1} = len M & ( for i being Nat st i in Seg (len M) holds

b_{1} . i = Sum (mlt ((Line (M,i)),F)) ) & len b_{2} = len M & ( for i being Nat st i in Seg (len M) holds

b_{2} . i = Sum (mlt ((Line (M,i)),F)) ) holds

b_{1} = b_{2}

end;
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 ( len it = len M & ( for i being Nat st i in Seg (len M) holds

it . i = Sum (mlt ((Line (M,i)),F)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines * MATRIXC1:def 6 :

for M being Matrix of COMPLEX

for F, b_{3} being FinSequence of COMPLEX holds

( b_{3} = M * F iff ( len b_{3} = len M & ( for i being Nat st i in Seg (len M) holds

b_{3} . i = Sum (mlt ((Line (M,i)),F)) ) ) );

for M being Matrix of COMPLEX

for F, b

( b

b

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)

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;

:: deftheorem defines * MATRIXC1:def 7 :

for M being Matrix of COMPLEX

for a being Complex holds M * a = a * M;

for M being Matrix of COMPLEX

for a being Complex holds M * a = a * M;

theorem :: MATRIXC1:17

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)

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

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)

for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)

proof end;

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

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) *'

addcomplex $$ (F *') = (addcomplex $$ F) *'

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

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

for a being Element of COMPLEX st len x = len y holds

mlt ((a * x),y) = a * (mlt (x,y))

proof end;

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

proof end;

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

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 ;

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)

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

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

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

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

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)

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)

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

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

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)) *'

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 *'))) *'

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 *')

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)

mlt (F1,(mlt (F2,F3))) = mlt ((mlt (F1,F2)),F3)

proof end;

definition

let M be Matrix of COMPLEX;

ex b_{1} being FinSequence of COMPLEX st

( len b_{1} = len M & ( for i being Nat st i in Seg (len M) holds

b_{1} . i = Sum (Line (M,i)) ) )

for b_{1}, b_{2} being FinSequence of COMPLEX st len b_{1} = len M & ( for i being Nat st i in Seg (len M) holds

b_{1} . i = Sum (Line (M,i)) ) & len b_{2} = len M & ( for i being Nat st i in Seg (len M) holds

b_{2} . i = Sum (Line (M,i)) ) holds

b_{1} = b_{2}

end;
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 ( len it = len M & ( for i being Nat st i in Seg (len M) holds

it . i = Sum (Line (M,i)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines LineSum MATRIXC1:def 9 :

for M being Matrix of COMPLEX

for b_{2} being FinSequence of COMPLEX holds

( b_{2} = LineSum M iff ( len b_{2} = len M & ( for i being Nat st i in Seg (len M) holds

b_{2} . i = Sum (Line (M,i)) ) ) );

for M being Matrix of COMPLEX

for b

( b

b

definition

let M be Matrix of COMPLEX;

ex b_{1} being FinSequence of COMPLEX st

( len b_{1} = width M & ( for j being Nat st j in Seg (width M) holds

b_{1} . j = Sum (Col (M,j)) ) )

for b_{1}, b_{2} being FinSequence of COMPLEX st len b_{1} = width M & ( for j being Nat st j in Seg (width M) holds

b_{1} . j = Sum (Col (M,j)) ) & len b_{2} = width M & ( for j being Nat st j in Seg (width M) holds

b_{2} . j = Sum (Col (M,j)) ) holds

b_{1} = b_{2}

end;
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 ( len it = width M & ( for j being Nat st j in Seg (width M) holds

it . j = Sum (Col (M,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines ColSum MATRIXC1:def 10 :

for M being Matrix of COMPLEX

for b_{2} being FinSequence of COMPLEX holds

( b_{2} = ColSum M iff ( len b_{2} = width M & ( for j being Nat st j in Seg (width M) holds

b_{2} . j = Sum (Col (M,j)) ) ) );

for M being Matrix of COMPLEX

for b

( b

b

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

for n being Nat st len f = n + 1 & g = f | n holds

Sum f = (Sum g) + (f /. (len f))

proof end;

:: deftheorem defines SumAll MATRIXC1:def 11 :

for M being Matrix of COMPLEX holds SumAll M = Sum (LineSum M);

for M being Matrix of COMPLEX holds SumAll M = Sum (LineSum M);

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 ;

ex b_{1} being Matrix of COMPLEX st

( len b_{1} = len x & width b_{1} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )

for b_{1}, b_{2} being Matrix of COMPLEX st len b_{1} = len x & width b_{1} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len b_{2} = len x & width b_{2} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) holds

b_{1} = b_{2}

end;
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 ( 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) *') ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being Matrix of COMPLEX holds

( b_{4} = QuadraticForm (x,M,y) iff ( len b_{4} = len x & width b_{4} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{4} * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) ) );

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

( b

b

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)) *'

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 *'))

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 Th53: :: MATRIXC1:55

for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds

|(x,y)| *' = |((x *'),(y *'))|

|(x,y)| *' = |((x *'),(y *'))|

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

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

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

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

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;