let x, y be FinSequence of COMPLEX ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: |((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)) ;
:: thesis: verum