let a, b, c, d, e, f be Real; 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)); 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; ( ( 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) )
; 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 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;
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;
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;
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;
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;
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;
( ( 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;
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) )
; verum