let a, b, c, d, e, f be Real; :: thesis: for P1, P2, P3, P4, P5, P6 being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P1 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) holds
ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
let P1, P2, P3, P4, P5, P6 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for N being invertible Matrix of 3,F_Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P1 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) holds
ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
let N be invertible Matrix of 3,F_Real; :: thesis: ( ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P1 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) implies ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) ) )
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: ( P1 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) ) ; :: thesis: ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
reconsider M1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) as Matrix of 3,REAL ;
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) as Matrix of 3,REAL by Lm03;
consider ra, rb, rc, rd, re, rf, rg, rh, ri being Element of F_Real such that
A3: MXR2MXF M2 = <*<*ra,rb,rc*>,<*rd,re,rf*>,<*rg,rh,ri*>*> by Th03;
MXR2MXF M2 is symmetric by Th14;
then A4: ( rb = rd & rc = rg & rf = rh ) by A3, Th06;
reconsider fa = ra, fe = re, fi = ri, fb = rb, fc = rc, ff = rf as Real ;
A5: M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) by A3, A4, MATRIXR1:def 1;
now :: thesis: ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
reconsider a2 = ra, b2 = re, c2 = ri, d2 = 2 * rb, e2 = 2 * rc, f2 = 2 * rf as Real ;
take a2 = a2; :: thesis: ex b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
take b2 = b2; :: thesis: ex c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
take c2 = c2; :: thesis: ex d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
take d2 = d2; :: thesis: ex e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
take e2 = e2; :: thesis: ex f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
take f2 = f2; :: thesis: ( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )
thus ( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) ) by A1, A2, A5, Th16; :: thesis: verum
end;
hence ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) ) ; :: thesis: verum