let x, y be FinSequence of REAL ; for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
let M be Matrix of REAL; ( len x = len M & len y = width M & len y > 0 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
and
A3:
len y > 0
; |(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
A4:
width (QuadraticForm (x,M,y)) = len y
by A1, A2, Def4;
A5:
len (LineSum (QuadraticForm (x,M,y))) = len (QuadraticForm (x,M,y))
by Th20;
len (M * y) = len x
by A1, A2, A3, MATRIXR1:61;
then A6: len (mlt (x,(M * y))) =
len x
by Th30
.=
len (LineSum (QuadraticForm (x,M,y)))
by A1, A2, A5, Def4
;
for i being Nat st 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) holds
(LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
proof
let i be
Nat;
( 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) implies (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i )
assume that A7:
1
<= i
and A8:
i <= len (LineSum (QuadraticForm (x,M,y)))
;
(LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
A9:
i in Seg (len (LineSum (QuadraticForm (x,M,y))))
by A7, A8;
then A10:
i in Seg (len M)
by A1, A2, A5, Def4;
then A11:
i in Seg (len (M * y))
by A2, A3, MATRIXR1:61;
A12:
len (Line (M,i)) = len y
by A2, MATRIX_0:def 7;
A13:
i <= len M
by A10, FINSEQ_1:1;
A14:
for
j being
Nat st 1
<= j &
j <= len (Line ((QuadraticForm (x,M,y)),i)) holds
((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j
proof
let j be
Nat;
( 1 <= j & j <= len (Line ((QuadraticForm (x,M,y)),i)) implies ((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j )
assume that A15:
1
<= j
and A16:
j <= len (Line ((QuadraticForm (x,M,y)),i))
;
((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j
j <= width M
by A2, A4, A16, MATRIX_0:def 7;
then A17:
[i,j] in Indices M
by A7, A13, A15, MATRIXC1:1;
j in Seg (len (Line ((QuadraticForm (x,M,y)),i)))
by A15, A16;
then A18:
j in Seg (width (QuadraticForm (x,M,y)))
by MATRIX_0:def 7;
thus ((x . i) * (mlt ((Line (M,i)),y))) . j =
(x . i) * ((mlt ((Line (M,i)),y)) . j)
by RVSUM_1:44
.=
(x . i) * (((Line (M,i)) . j) * (y . j))
by RVSUM_1:59
.=
(x . i) * ((M * (i,j)) * (y . j))
by A2, A4, A18, MATRIX_0:def 7
.=
((x . i) * (M * (i,j))) * (y . j)
.=
(QuadraticForm (x,M,y)) * (
i,
j)
by A1, A2, A17, Def4
.=
(Line ((QuadraticForm (x,M,y)),i)) . j
by A18, MATRIX_0:def 7
;
verum
end;
A19:
len (Line ((QuadraticForm (x,M,y)),i)) = len y
by A4, MATRIX_0:def 7;
len (mlt ((Line (M,i)),y)) = len y
by A12, Th30;
then
len ((x . i) * (mlt ((Line (M,i)),y))) = len (Line ((QuadraticForm (x,M,y)),i))
by A19, RVSUM_1:117;
then A20:
(x . i) * (mlt ((Line (M,i)),y)) = Line (
(QuadraticForm (x,M,y)),
i)
by A14;
(mlt (x,(M * y))) . i =
(x . i) * ((M * y) . i)
by RVSUM_1:59
.=
(x . i) * ((Line (M,i)) "*" y)
by A2, A3, A11, Th41
.=
Sum ((x . i) * (mlt ((Line (M,i)),y)))
by RVSUM_1:87
;
hence
(LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
by A5, A9, A20, Th20;
verum
end;
hence
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
by A6, FINSEQ_1:14; verum