let x, y be FinSequence of REAL ; for M being Matrix of REAL st len x = len M & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))
let M be Matrix of REAL; ( len x = len M & len y = width M implies |((x * M),y)| = SumAll (QuadraticForm (x,M,y)) )
set Z = QuadraticForm (x,M,y);
assume that
A1:
len x = len M
and
A2:
len y = width M
; |((x * M),y)| = SumAll (QuadraticForm (x,M,y))
A3:
len (QuadraticForm (x,M,y)) = len x
by A1, A2, Def4;
A4:
len (ColSum (QuadraticForm (x,M,y))) = width (QuadraticForm (x,M,y))
by Def2;
len (x * M) = len y
by A1, A2, MATRIXR1:62;
then A5: len (mlt ((x * M),y)) =
len y
by Th30
.=
len (ColSum (QuadraticForm (x,M,y)))
by A1, A2, A4, Def4
;
for i being Nat st 1 <= i & i <= len (ColSum (QuadraticForm (x,M,y))) holds
(ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i
proof
let i be
Nat;
( 1 <= i & i <= len (ColSum (QuadraticForm (x,M,y))) implies (ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i )
assume that A6:
1
<= i
and A7:
i <= len (ColSum (QuadraticForm (x,M,y)))
;
(ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i
A8:
i in Seg (len (ColSum (QuadraticForm (x,M,y))))
by A6, A7;
then A9:
i in Seg (width M)
by A1, A2, A4, Def4;
then A10:
i in Seg (len (x * M))
by A1, MATRIXR1:62;
A11:
len (Col (M,i)) = len x
by A1, MATRIX_0:def 8;
A12:
i <= width M
by A9, FINSEQ_1:1;
A13:
for
j being
Nat st 1
<= j &
j <= len (Col ((QuadraticForm (x,M,y)),i)) holds
((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j
proof
let j be
Nat;
( 1 <= j & j <= len (Col ((QuadraticForm (x,M,y)),i)) implies ((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j )
assume that A14:
1
<= j
and A15:
j <= len (Col ((QuadraticForm (x,M,y)),i))
;
((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j
j <= len M
by A1, A3, A15, MATRIX_0:def 8;
then A16:
[j,i] in Indices M
by A6, A12, A14, MATRIXC1:1;
j in Seg (len (Col ((QuadraticForm (x,M,y)),i)))
by A14, A15;
then A17:
j in Seg (len (QuadraticForm (x,M,y)))
by MATRIX_0:def 8;
then A18:
j in dom (QuadraticForm (x,M,y))
by FINSEQ_1:def 3;
A19:
j in dom M
by A1, A3, A17, FINSEQ_1:def 3;
thus ((y . i) * (mlt (x,(Col (M,i))))) . j =
(y . i) * ((mlt (x,(Col (M,i)))) . j)
by RVSUM_1:44
.=
(y . i) * ((x . j) * ((Col (M,i)) . j))
by RVSUM_1:59
.=
(y . i) * ((x . j) * (M * (j,i)))
by A19, MATRIX_0:def 8
.=
(QuadraticForm (x,M,y)) * (
j,
i)
by A1, A2, A16, Def4
.=
(Col ((QuadraticForm (x,M,y)),i)) . j
by A18, MATRIX_0:def 8
;
verum
end;
A20:
len (Col ((QuadraticForm (x,M,y)),i)) = len x
by A3, MATRIX_0:def 8;
len (mlt (x,(Col (M,i)))) = len x
by A11, Th30;
then
len ((y . i) * (mlt (x,(Col (M,i))))) = len (Col ((QuadraticForm (x,M,y)),i))
by A20, RVSUM_1:117;
then A21:
(y . i) * (mlt (x,(Col (M,i)))) = Col (
(QuadraticForm (x,M,y)),
i)
by A13;
(mlt ((x * M),y)) . i =
((x * M) . i) * (y . i)
by RVSUM_1:59
.=
(x "*" (Col (M,i))) * (y . i)
by A1, A10, Th40
.=
Sum ((y . i) * (mlt (x,(Col (M,i)))))
by RVSUM_1:87
;
hence
(ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i
by A4, A8, A21, Def2;
verum
end;
hence |((x * M),y)| =
Sum (ColSum (QuadraticForm (x,M,y)))
by A5, FINSEQ_1:14
.=
SumAll (QuadraticForm (x,M,y))
by Th29
;
verum