let p be FinSequence of REAL ; :: thesis:
let a, b, c, d, e, f be Real; :: thesis:
let u be Point of (TOP-REAL 3); :: thesis:
let M be Matrix of 3,REAL; :: thesis:
assume that
A1: p = u and
A2: M = symmetric_3 (a,b,c,d,e,f) ; :: thesis:
reconsider ru = u as Element of REAL 3 by EUCLID:22;
A3: MXR2MXF (ColVec2Mx p) = <*ru*> @ by A1, ANPROJ_8:72;
reconsider a = a, b = b, c = c, d = d, e = e, f = f as Element of F_Real by XREAL_0:def 1;
reconsider fu1 = ru . 1, fu2 = ru . 2, fu3 = ru . 3 as Element of F_Real by XREAL_0:def 1;
A4: <*ru*> @ = <*<*fu1*>,<*fu2*>,<*fu3*>*> by EUCLID_8:50, ANPROJ_8:77;
A5: len ru = 3 by EUCLID_8:50;
A6: len <*ru*> = 1 by FINSEQ_1:39;
rng <*ru*> = {ru} by FINSEQ_1:39;
then ru in rng <*ru*> by TARSKI:def 1;
then A7: width <*ru*> = 3 by A5, A6, MATRIX_0:def 3;
then A8: width (<*ru*> @) = len <*ru*> by MATRIX_0:29
.= 1 by FINSEQ_1:39 ;
A9: len (<*ru*> @) = 3 by MATRIX_0:def 6, A7;
then A10: <*ru*> @ is Matrix of 3,1,F_Real by A8, MATRIX_0:20;
reconsider M2 = <*ru*> @ as Matrix of 3,1,F_Real by A9, A8, MATRIX_0:20;
A11: M * (ColVec2Mx p) = M * (<*ru*> @) by A3, MATRIXR1:def 1
.= MXF2MXR ((MXR2MXF M) * (MXR2MXF (<*ru*> @))) by MATRIXR1:def 6 ;
A12: MXR2MXF (<*ru*> @) is Matrix of 3,1,F_Real by MATRIXR1:def 1, A10;
A13: MXR2MXF (<*ru*> @) = <*<*fu1*>,<*fu2*>,<*fu3*>*> by A4, MATRIXR1:def 1;
A14: (MXR2MXF M) * (MXR2MXF (<*ru*> @)) = <*<*(((a * fu1) + (d * fu2)) + (e * fu3))*>,<*(((d * fu1) + (b * fu2)) + (f * fu3))*>,<*(((e * fu1) + (f * fu2)) + (c * fu3))*>*> by A12, A2, MATRIXR1:def 1, A13, ANPROJ_9:7;
reconsider q = <*(((a * fu1) + (d * fu2)) + (e * fu3)),(((d * fu1) + (b * fu2)) + (f * fu3)),(((e * fu1) + (f * fu2)) + (c * fu3))*> as FinSequence of REAL ;
A15: ( q . 1 = ((a * fu1) + (d * fu2)) + (e * fu3) & q . 2 = ((d * fu1) + (b * fu2)) + (f * fu3) & q . 3 = ((e * fu1) + (f * fu2)) + (c * fu3) ) by FINSEQ_1:45;
A16: |[(((a * (u . 1)) + (d * (u . 2))) + (e * (u . 3))),(((d * (u . 1)) + (b * (u . 2))) + (f * (u . 3))),(((e * (u . 1)) + (f * (u . 2))) + (c * (u . 3)))]| in TOP-REAL 3 ;
then reconsider rq = q as Element of REAL 3 by EUCLID:22;
reconsider qf = q as FinSequence of F_Real ;
A17: len q = 3 by FINSEQ_1:45;
A18: ColVec2Mx rq = MXR2MXF (ColVec2Mx rq) by MATRIXR1:def 1
.= <*qf*> @ by ANPROJ_8:72 ;
then A19: ColVec2Mx rq = F2M q by A17, ANPROJ_8:88
.= <*<*(((a * fu1) + (d * fu2)) + (e * fu3))*>,<*(((d * fu1) + (b * fu2)) + (f * fu3))*>,<*(((e * fu1) + (f * fu2)) + (c * fu3))*>*> by A15, A17, ANPROJ_8:def 1
.= M * (ColVec2Mx p) by A14, A11, MATRIXR1:def 2 ;
A20: M * p = Col ((ColVec2Mx rq),1) by A19, MATRIXR1:def 11
.= <*(((a * fu1) + (d * fu2)) + (e * fu3)),(((d * fu1) + (b * fu2)) + (f * fu3)),(((e * fu1) + (f * fu2)) + (c * fu3))*> by A18, ANPROJ_8:93 ;
then A21: ( (M * p) . 1 = ((a * fu1) + (d * fu2)) + (e * fu3) & (M * p) . 2 = ((d * fu1) + (b * fu2)) + (f * fu3) & (M * p) . 3 = ((e * fu1) + (f * fu2)) + (c * fu3) ) by FINSEQ_1:45;
A22: ( len M = 3 & width M = 3 ) by MATRIX_0:24;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A23: len p = 3 by A1, EUCLID_8:50;
reconsider Mp = M * p as Element of REAL 3 by A16, A20, EUCLID:22;
|(p,(M * p))| = (((ru . 1) * (Mp . 1)) + ((ru . 2) * (Mp . 2))) + ((ru . 3) * (Mp . 3)) by A1, EUCLID_8:63
.= qfconic (a,b,c,(2 * d),(2 * e),(2 * f),u) by A21 ;
hence SumAll (QuadraticForm (p,M,p)) = qfconic (a,b,c,(2 * d),(2 * e),(2 * f),u) by A23, A22, MATRPROB:44; :: thesis: