let a, b, c, d, e, f be Real; :: thesis:
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
let N be invertible Matrix of 3,F_Real; :: thesis:
assume that
A1: ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) and
A2: P in conic (a,b,c,d,e,f) ; :: thesis:
consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A3: P = Q and
A4: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 by A2;
reconsider M = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) as Matrix of 3,REAL ;
A5: MXR2MXF M = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) by MATRIXR1:def 1;
consider uh, vh being Element of (TOP-REAL 3), ufh being FinSequence of F_Real, ph being FinSequence of 1 -tuples_on REAL such that
A6: ( P = Dir uh & not uh is zero & uh = ufh & ph = N * ufh & vh = M2F ph & not vh is zero & (homography N) . P = Dir vh ) by ANPROJ_8:def 4;
reconsider pR = uh as FinSequence of REAL by EUCLID:24;
A7: SumAll (QuadraticForm (pR,M,pR)) = qfconic (a,b,c,(2 * (d / 2)),(2 * (e / 2)),(2 * (f / 2)),uh) by Th13
.= 0 by A3, A4, A6 ;
reconsider x = uh `1 , y = uh `2 , z = uh `3 as Element of F_Real by XREAL_0:def 1;
A8: ufh = <*x,y,z*> by A6, EUCLID_5:27;
consider an, bn, cn, dn, en, fn, gn, hn, iN being Element of F_Real such that
A9: N = <*<*an,bn,cn*>,<*dn,en,fn*>,<*gn,hn,iN*>*> by Th03;
reconsider uf = ufh as FinSequence of REAL ;
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) as Matrix of 3,REAL by Lm03;
reconsider T = MXF2MXR ((MXR2MXF (NR @)) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
T * M is Matrix of 3,REAL ;
then reconsider M3 = (MXF2MXR ((MXR2MXF (NR @)) ~)) * M, M4 = MXF2MXR ((MXR2MXF NR) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M5 = (MXR2MXF (NR @)) ~ as Matrix of 3,F_Real ;
reconsider M6 = MXF2MXR M5 as Matrix of 3,REAL by MATRIXR1:def 2;
NR @ is invertible by Lm12;
then A10: MXR2MXF (NR @) is invertible by Lm15;
(MXR2MXF (NR @)) @ = MXR2MXF NR

reconsider N1 = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
A11: NR @ = N @ by MATRIXR1:def 2;
reconsider N2 = MXR2MXF (NR @) as Matrix of 3,F_Real ;
A12: ( len N = 3 & width N = 3 ) by MATRIX_0:24;
(MXR2MXF (NR @)) @ = (N @) @ by A11, MATRIXR1:def 1
.= N by A12, MATRIX_0:57 ;
hence (MXR2MXF (NR @)) @ = MXR2MXF NR by ANPROJ_8:16; :: thesis:

end;

then A13: M5 @ = (MXR2MXF NR) ~ by A10, MATRIX14:31;
A14: MXR2MXF M2 is symmetric

proof

A15: ( len M5 = 3 & width M5 = 3 ) by MATRIX_0:24;
MXR2MXF M2 = (MXR2MXF M3) * (MXR2MXF M4) by Lm07
.= (MXR2MXF (M6 * M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~)))
.= ((MXR2MXF (MXF2MXR M5)) * (MXR2MXF M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~))) by Lm07
.= (M5 * (MXR2MXF M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~))) by ANPROJ_8:16
.= (M5 * (MXR2MXF M)) * ((MXR2MXF NR) ~) by ANPROJ_8:16
.= (((M5 @) @) * (MXR2MXF M)) * (M5 @) by A13, A15, MATRIX_0:57 ;
hence MXR2MXF M2 is symmetric by A5, Th12, Th07; :: thesis:

end;

consider ma, mb, mc, md, me, mf, mg, mh, mi being Element of F_Real such that
A16: M2 = <*<*ma,mb,mc*>,<*md,me,mf*>,<*mg,mh,mi*>*> by Th03;
MXR2MXF M2 = <*<*ma,mb,mc*>,<*md,me,mf*>,<*mg,mh,mi*>*> by A16, MATRIXR1:def 1;
then A17: ( mb = md & mc = mg & mh = mf ) by A14, Th06;
uh in TOP-REAL 3 ;
then uh in REAL 3 by EUCLID:22;
then A18: len uf = 3 by A6, EUCLID_8:50;
A19: ( len (((NR @) * M2) * NR) = 3 & width (((NR @) * M2) * NR) = 3 ) by MATRIX_0:24;
A20: |((NR * uf),(M2 * (NR * uf)))| = |(uf,((((NR @) * M2) * NR) * uf))| by A18, Lm02
.= SumAll (QuadraticForm (uf,(((NR @) * M2) * NR),uf)) by A18, A19, MATRPROB:44
.= 0 by A6, A7, Lm13 ;
width NR = 3 by MATRIX_0:24;
then len (NR * uf) = len NR by A18, MATRIXR1:61;
then A21: len (NR * uf) = 3 by MATRIX_0:24;
then ( len (NR * uf) = len M2 & len (NR * uf) = width M2 & len (NR * uf) > 0 ) by MATRIX_0:24;
then A22: SumAll (QuadraticForm ((NR * uf),M2,(NR * uf))) = 0 by A20, MATRPROB:44;
reconsider u3 = NR * uf as Element of (TOP-REAL 3) by A21, EUCLID:76;
not u3 is zero

proof

assume A23: u3 is zero ; :: thesis:
reconsider p = 0. (TOP-REAL 3) as FinSequence of REAL by EUCLID:24;
A24: ( width NR = 3 & width (Inv NR) = 3 & len NR = 3 ) by MATRIX_0:24;
A25: NR is invertible by Lm14;
(Inv NR) * p = ((Inv NR) * NR) * uf by A23, A24, A18, MATRIXR2:59
.= (1_Rmatrix 3) * uf by A25, MATRIXR2:def 6
.= uf by A18, MATRIXR2:86 ;
hence contradiction by Lm16, A6; :: thesis:

end;

then reconsider u2 = NR * uf as non zero Element of (TOP-REAL 3) ;
reconsider fa = ma, fb = mb, fc = mc, fe = me, ff = mf, fi = mi as Real ;
M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) by A16, A17;
then A26: qfconic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff),u2) = 0 by A22, Th13;
A27: ( not fa = 0 or not fe = 0 or not fi = 0 or not 2 * fb = 0 or not 2 * ff = 0 or not 2 * fc = 0 )

proof

assume A28: ( fa = 0 & fe = 0 & fi = 0 & 2 * fb = 0 & 2 * ff = 0 & 2 * fc = 0 ) ; :: thesis:
A29: ((NR @) * (0_Rmatrix 3)) * NR = (0_Rmatrix 3) * NR by Lm20
.= 0_Rmatrix 3 by Lm20 ;
reconsider z1 = 0 , z2 = 0 , z3 = 0 , z4 = 0 , z5 = 0 , z6 = 0 , z7 = 0 , z8 = 0 , z9 = 0 , a1 = a, b1 = b, c1 = c, d1 = d / 2, e1 = f / 2, f1 = e / 2 as Element of F_Real by XREAL_0:def 1;
<*<*a1,d1,f1*>,<*d1,b1,e1*>,<*f1,e1,c1*>*> = <*<*z1,z2,z3*>,<*z4,z5,z6*>,<*z7,z8,z9*>*> by A29, Lm13, A28, A17, A16, Lm18;
then ( a1 = z1 & b1 = z5 & c1 = z9 & d1 = z2 & e1 = z5 & f1 = z3 ) by Th02;
hence contradiction by A1; :: thesis:

end;

A30: u2 = vh

proof

( ph = <*<*(((an * x) + (bn * y)) + (cn * z))*>,<*(((dn * x) + (en * y)) + (fn * z))*>,<*(((gn * x) + (hn * y)) + (iN * z))*>*> & vh = <*(((an * x) + (bn * y)) + (cn * z)),(((dn * x) + (en * y)) + (fn * z)),(((gn * x) + (hn * y)) + (iN * z))*> ) by A6, A8, A9, Th08;
hence u2 = vh by A8, Th09, A9, MATRIXR1:def 2; :: thesis:

end;

for ufa, ufb, ufc, ufd, ufe, ufi, uff being Real
for UM1, UM2, UNR being Matrix of 3,REAL st UM1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) & UNR = MXF2MXR N & UM2 = ((MXF2MXR ((MXR2MXF (UNR @)) ~)) * UM1) * (MXF2MXR ((MXR2MXF UNR) ~)) & UM2 = symmetric_3 (ufa,ufe,ufi,ufb,ufc,uff) holds
( ( not ufa = 0 or not ufe = 0 or not ufi = 0 or not ufb = 0 or not uff = 0 or not ufc = 0 ) & (homography N) . P in conic (ufa,ufe,ufi,(2 * ufb),(2 * ufc),(2 * uff)) )

proof

let ufa, ufb, ufc, ufd, ufe, ufi, uff be Real; :: thesis:
let UM1, UM2 be Matrix of 3,REAL; :: thesis:
let UNR be Matrix of 3,REAL; :: thesis:
assume that
A31: UM1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) and
A32: UNR = MXF2MXR N and
A33: UM2 = ((MXF2MXR ((MXR2MXF (UNR @)) ~)) * UM1) * (MXF2MXR ((MXR2MXF UNR) ~)) and
A34: UM2 = symmetric_3 (ufa,ufe,ufi,ufb,ufc,uff) ; :: thesis:
symmetric_3 (ufa,ufe,ufi,ufb,ufc,uff) = symmetric_3 (fa,fe,fi,fb,fc,ff) by A31, A32, A33, A34, A16, A17;
then ( fa = ufa & fb = ufb & fc = ufc & fe = ufe & ff = uff & fi = ufi ) by Th15;
hence ( ( not ufa = 0 or not ufe = 0 or not ufi = 0 or not ufb = 0 or not uff = 0 or not ufc = 0 ) & (homography N) . P in conic (ufa,ufe,ufi,(2 * ufb),(2 * ufc),(2 * uff)) ) by A27, A30, A26, A6, Th11; :: thesis:

end;

hence for fa, fb, fc, fd, fe, fi, ff being Real
for M1, M2, NR being Matrix of 3,REAL st M1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) & NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) & M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) holds
( ( not fa = 0 or not fe = 0 or not fi = 0 or not fb = 0 or not ff = 0 or not fc = 0 ) & (homography N) . P in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) ) ; :: thesis: