let x, y be 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))
let M be Matrix of COMPLEX; ( len y = len M & len x = width M & len x > 0 & len y > 0 implies |((M * x),y)| = SumAll (QuadraticForm (x,(M @),y)) )
assume that
A1:
len y = len M
and
A2:
len x = width M
and
A3:
len x > 0
and
A4:
len y > 0
; |((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))
A5:
(M @) @" = M *'
by A1, A2, A3, A4, MATRIX_0:57;
A6:
width (M @) = len M
by A2, A3, MATRIX_0:54;
A7:
len (x *') = width M
by A2, COMPLSP2:def 1;
len (y *') = len M
by A1, COMPLSP2:def 1;
then A8:
len (QuadraticForm ((y *'),M,(x *'))) = len M
by A7, Def12;
A9:
len (x *') = len x
by COMPLSP2:def 1;
A10:
0 + 1 <= len x
by A3, NAT_1:13;
A11:
len (y *') = len y
by COMPLSP2:def 1;
A12:
len (M @) = width M
by MATRIX_0:def 6;
A13:
len (M * x) = len M
by Def6;
hence |((M * x),y)| =
|(y,(M * x))| *'
by A1, A4, Th52
.=
|((y *'),((M * x) *'))|
by A1, A4, A13, Th53
.=
|((y *'),((M *') * (x *')))|
by A2, A10, Th41
.=
SumAll (QuadraticForm ((y *'),((M @) @),(x *')))
by A1, A2, A3, A4, A9, A11, A12, A6, A5, Th55
.=
SumAll (QuadraticForm ((y *'),M,(x *')))
by A1, A2, A3, A4, MATRIX_0:57
.=
SumAll ((QuadraticForm ((y *'),M,(x *'))) @)
by A1, A4, A8, Th49
.=
SumAll ((QuadraticForm ((x *'),(M @"),(y *'))) *')
by A1, A2, A3, A9, A11, Th50
.=
SumAll (((QuadraticForm (x,(M @),y)) *') *')
by A1, A2, A12, A6, Th51
.=
SumAll (QuadraticForm (x,(M @),y))
;
verum