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_2:15;
A6: width (M @ ) = len M by A2, A3, MATRIX_2:12;
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, Def13;
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_1:def 7;
A13: len (M * x) = len M by Def7;
hence |((M * x),y)| = |(y,(M * x))| *' by A1, A4, Th57
.= |((y *' ),((M * x) *' ))| by A1, A4, A13, Th58
.= |((y *' ),((M *' ) * (x *' )))| by A2, A10, Th45
.= SumAll (QuadraticForm (y *' ),((M @ ) @ ),(x *' )) by A1, A2, A3, A4, A9, A11, A12, A6, A5, Th60
.= SumAll (QuadraticForm (y *' ),M,(x *' )) by A1, A2, A3, A4, MATRIX_2:15
.= SumAll ((QuadraticForm (y *' ),M,(x *' )) @ ) by A1, A4, A8, Th54
.= SumAll ((QuadraticForm (x *' ),(M @" ),(y *' )) *' ) by A1, A2, A3, A9, A11, Th55
.= SumAll (((QuadraticForm x,(M @ ),y) *' ) *' ) by A1, A2, A12, A6, Th56
.= SumAll (QuadraticForm x,(M @ ),y) by Th2 ;
:: thesis: verum