let x, y be FinSequence of COMPLEX ; for M being Matrix of COMPLEX st len x = width M & len y = len M & len x > 0 & len y > 0 holds
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
let M be Matrix of COMPLEX; ( len x = width M & len y = len M & len x > 0 & len y > 0 implies |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) )
assume that
A1:
len x = width M
and
A2:
len y = len M
and
A3:
len x > 0
and
A4:
len y > 0
; |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
A5:
width (M @) = len y
by A1, A2, A3, MATRIX_0:54;
then A6:
width ((M @) *') = len y
by Def1;
A7: dom (LineSum (QuadraticForm (x,(M @),y))) =
Seg (len (LineSum (QuadraticForm (x,(M @),y))))
by FINSEQ_1:def 3
.=
Seg (len (QuadraticForm (x,(M @),y)))
by Def9
;
A8:
len (M @) = len x
by A1, MATRIX_0:def 6;
A9: len (LineSum (QuadraticForm (x,(M @),y))) =
len (QuadraticForm (x,(M @),y))
by Def9
.=
len x
by A8, A5, Def12
;
A10: len (M @") =
len (M @)
by Def1
.=
len x
by A1, MATRIX_0:def 6
;
then A11:
len ((M @") * y) = len x
by Def6;
then
len (((M @") * y) *') = len x
by COMPLSP2:def 1;
then A12:
len (LineSum (QuadraticForm (x,(M @),y))) = len (mlt (x,(((M @") * y) *')))
by A9, FINSEQ_2:72;
A13:
0 + 1 <= len y
by A4, NAT_1:13;
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 A14:
1
<= i
and A15:
i <= len (LineSum (QuadraticForm (x,(M @),y)))
;
(LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i
A16:
len y =
width (QuadraticForm (x,(M @),y))
by A8, A5, Def12
.=
len (Line ((QuadraticForm (x,(M @),y)),i))
by MATRIX_0:def 7
;
A17:
len (Line ((M @"),i)) = len y
by A6, MATRIX_0:def 7;
then A18:
len (mlt ((Line ((M @"),i)),y)) >= 1
by A13, FINSEQ_2:72;
len (M @) = len (QuadraticForm (x,(M @),y))
by A8, A5, Def12;
then A19:
len (M @) = len (LineSum (QuadraticForm (x,(M @),y)))
by Def9;
then A20:
i in Seg (len (M @"))
by A8, A10, A14, A15, FINSEQ_1:1;
A21:
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
A22:
len (Line ((M @),i)) =
width (M @)
by MATRIX_0:def 7
.=
len y
by A1, A2, A3, MATRIX_0:54
.=
len (y *')
by COMPLSP2:def 1
;
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 A23:
1
<= j
and A24:
j <= len (Line ((QuadraticForm (x,(M @),y)),i))
;
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j
A25:
j in Seg (width (M @))
by A5, A16, A23, A24, FINSEQ_1:1;
j in Seg (len y)
by A16, A23, A24, FINSEQ_1:1;
then
j in Seg (len (y *'))
by COMPLSP2:def 1;
then
j in Seg (len (mlt ((Line ((M @),i)),(y *'))))
by A22, FINSEQ_2:72;
then A26:
j in dom (mlt ((Line ((M @),i)),(y *')))
by FINSEQ_1:def 3;
j in Seg (len (Line ((QuadraticForm (x,(M @),y)),i)))
by A23, A24, FINSEQ_1:1;
then A27:
j in Seg (width (QuadraticForm (x,(M @),y)))
by MATRIX_0:def 7;
j <= width (M @)
by A1, A2, A3, A16, A24, MATRIX_0:54;
then A28:
[i,j] in Indices (M @)
by A14, A15, A19, A23, Th1;
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j =
(x . i) * (((mlt ((Line ((M @"),i)),y)) *') . j)
by COMPLSP2:16
.=
(x . i) * ((mlt (((Line ((M @"),i)) *'),(y *'))) . j)
by A17, Th25
.=
(x . i) * ((mlt ((Line ((M @),i)),(y *'))) . j)
by A8, A10, A20, Th39
.=
(x . i) * (((Line ((M @),i)) . j) * ((y *') . j))
by A26, Th17
.=
(x . i) * (((Line ((M @),i)) . j) * ((y . j) *'))
by A16, A23, A24, COMPLSP2:def 1
.=
((x . i) * ((Line ((M @),i)) . j)) * ((y . j) *')
.=
((x . i) * ((M @) * (i,j))) * ((y . j) *')
by A25, MATRIX_0:def 7
.=
(QuadraticForm (x,(M @),y)) * (
i,
j)
by A8, A5, A28, Def12
;
hence
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j
by A27, MATRIX_0:def 7;
verum
end;
i in Seg (len (LineSum (QuadraticForm (x,(M @),y))))
by A14, A15, FINSEQ_1:1;
then A29:
i in dom (LineSum (QuadraticForm (x,(M @),y)))
by FINSEQ_1:def 3;
A30:
len (Line ((M @"),i)) = len y
by A6, MATRIX_0:def 7;
A31:
len ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) =
len ((mlt ((Line ((M @"),i)),y)) *')
by COMPLSP2:3
.=
len (mlt ((Line ((M @"),i)),y))
by COMPLSP2:def 1
.=
len (Line ((QuadraticForm (x,(M @),y)),i))
by A16, A30, FINSEQ_2:72
;
i in Seg (len (mlt (x,(((M @") * y) *'))))
by A12, A14, A15, FINSEQ_1:1;
then
i in dom (mlt (x,(((M @") * y) *')))
by FINSEQ_1:def 3;
then (mlt (x,(((M @") * y) *'))) . i =
(x . i) * ((((M @") * y) *') . i)
by Th17
.=
(x . i) * ((((M @") * y) . i) *')
by A11, A9, A14, A15, COMPLSP2:def 1
;
then (mlt (x,(((M @") * y) *'))) . i =
(x . i) * ((Sum (mlt ((Line ((M @"),i)),y))) *')
by A20, Def6
.=
(x . i) * (Sum ((mlt ((Line ((M @"),i)),y)) *'))
by A18, Th21
.=
Sum ((x . i) * ((mlt ((Line ((M @"),i)),y)) *'))
by Th26
;
then
(mlt (x,(((M @") * y) *'))) . i = Sum (Line ((QuadraticForm (x,(M @),y)),i))
by A31, A21, FINSEQ_1:14;
hence
(LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i
by A7, A29, Def9;
verum
end;
then
Sum (LineSum (QuadraticForm (x,(M @),y))) = Sum (mlt (x,(((M @") * y) *')))
by A12, FINSEQ_1:14;
hence
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
by A11, Th37; verum