let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3)); for a, b, c, d, e, f being 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,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P7,P2,P5 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear holds
P7,P8,P9 are_collinear
let a, b, c, d, e, f be 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,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P7,P2,P5 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear implies P7,P8,P9 are_collinear )
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,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f)
and
A3:
not P1,P2,P3 are_collinear
and
A4:
not P1,P2,P4 are_collinear
and
A5:
not P1,P3,P4 are_collinear
and
A6:
not P2,P3,P4 are_collinear
and
A7:
not P7,P2,P5 are_collinear
and
A8:
not P1,P2,P5 are_collinear
and
A9:
not P1,P2,P6 are_collinear
and
A10:
not P1,P3,P5 are_collinear
and
A11:
not P1,P3,P6 are_collinear
and
A12:
not P1,P5,P7 are_collinear
and
A13:
not P2,P4,P5 are_collinear
and
A14:
not P2,P4,P6 are_collinear
and
A15:
not P2,P4,P7 are_collinear
and
A16:
not P2,P5,P9 are_collinear
and
A17:
not P2,P6,P8 are_collinear
and
A18:
not P2,P7,P8 are_collinear
and
A19:
not P2,P7,P9 are_collinear
and
A20:
not P3,P4,P5 are_collinear
and
A21:
not P3,P4,P6 are_collinear
and
A22:
not P3,P5,P8 are_collinear
and
A23:
not P3,P6,P8 are_collinear
and
A24:
not P5,P7,P8 are_collinear
and
A25:
not P5,P7,P9 are_collinear
and
A26:
P1,P5,P9 are_collinear
and
A27:
P1,P6,P8 are_collinear
and
A28:
P2,P4,P9 are_collinear
and
A29:
P2,P6,P7 are_collinear
and
A30:
P3,P4,P8 are_collinear
and
A31:
P3,P5,P7 are_collinear
; P7,P8,P9 are_collinear
consider N being invertible Matrix of 3,F_Real such that
A32:
(homography N) . P1 = Dir100
and
A33:
(homography N) . P2 = Dir010
and
A34:
(homography N) . P3 = Dir001
and
A35:
(homography N) . P4 = Dir111
by A3, A4, A5, A6, ANPROJ_9:30;
consider u5 being Point of (TOP-REAL 3) such that
A36:
not u5 is zero
and
A37:
(homography N) . P5 = Dir u5
by ANPROJ_1:26;
reconsider p51 = u5 . 1, p52 = u5 . 2, p53 = u5 . 3 as Real ;
A38:
( u5 `1 = u5 . 1 & u5 `2 = u5 . 2 & u5 `3 = u5 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A39:
(homography N) . P5 = Dir |[p51,p52,p53]|
by A37, EUCLID_5:3;
consider u6 being Point of (TOP-REAL 3) such that
A40:
not u6 is zero
and
A41:
(homography N) . P6 = Dir u6
by ANPROJ_1:26;
reconsider p61 = u6 . 1, p62 = u6 . 2, p63 = u6 . 3 as Real ;
A42:
( u6 `1 = u6 . 1 & u6 `2 = u6 . 2 & u6 `3 = u6 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A43:
(homography N) . P6 = Dir |[p61,p62,p63]|
by A41, EUCLID_5:3;
consider u7 being Point of (TOP-REAL 3) such that
A44:
not u7 is zero
and
A45:
(homography N) . P7 = Dir u7
by ANPROJ_1:26;
reconsider p71 = u7 . 1, p72 = u7 . 2, p73 = u7 . 3 as Real ;
A46:
( u7 `1 = u7 . 1 & u7 `2 = u7 . 2 & u7 `3 = u7 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A47:
(homography N) . P7 = Dir |[p71,p72,p73]|
by A45, EUCLID_5:3;
consider u8 being Point of (TOP-REAL 3) such that
A48:
not u8 is zero
and
A49:
(homography N) . P8 = Dir u8
by ANPROJ_1:26;
reconsider p81 = u8 . 1, p82 = u8 . 2, p83 = u8 . 3 as Real ;
A50:
( u8 `1 = u8 . 1 & u8 `2 = u8 . 2 & u8 `3 = u8 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A51:
(homography N) . P8 = Dir |[p81,p82,p83]|
by A49, EUCLID_5:3;
consider u9 being Point of (TOP-REAL 3) such that
A52:
not u9 is zero
and
A53:
(homography N) . P9 = Dir u9
by ANPROJ_1:26;
reconsider p91 = u9 . 1, p92 = u9 . 2, p93 = u9 . 3 as Real ;
A54:
( u9 `1 = u9 . 1 & u9 `2 = u9 . 2 & u9 `3 = u9 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A55:
(homography N) . P9 = Dir |[p91,p92,p93]|
by A53, EUCLID_5:3;
A56:
( P1 in {P1,P2,P3,P4,P5,P6} & P2 in {P1,P2,P3,P4,P5,P6} & P3 in {P1,P2,P3,P4,P5,P6} & P4 in {P1,P2,P3,P4,P5,P6} & P5 in {P1,P2,P3,P4,P5,P6} & P6 in {P1,P2,P3,P4,P5,P6} )
by ENUMSET1:def 4;
consider a2, b2, c2, d2, e2, f2 being Real such that
A57:
( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 )
and
A58:
(homography N) . P1 in conic (a2,b2,c2,d2,e2,f2)
and
A59:
(homography N) . P2 in conic (a2,b2,c2,d2,e2,f2)
and
A60:
(homography N) . P3 in conic (a2,b2,c2,d2,e2,f2)
and
A61:
(homography N) . P4 in conic (a2,b2,c2,d2,e2,f2)
and
A62:
(homography N) . P5 in conic (a2,b2,c2,d2,e2,f2)
and
A63:
(homography N) . P6 in conic (a2,b2,c2,d2,e2,f2)
by A56, A2, A1, Th17;
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A64:
Dir |[1,0,0]| = P
and
A65:
for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0
by A32, A58;
A66:
( qfconic (a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
proof
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[1,0,0]|)
= 0
by A64, A65, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A67:
Dir |[0,1,0]| = P
and A68:
for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
u)
= 0
by A33, A59;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[0,1,0]|)
= 0
by A67, A68, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A69:
Dir |[0,0,1]| = P
and A70:
for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
u)
= 0
by A34, A60;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[0,0,1]|)
= 0
by A69, A70, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A71:
Dir |[1,1,1]| = P
and A72:
for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
u)
= 0
by A35, A61;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[1,1,1]|)
= 0
by A71, A72, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A73:
Dir |[p51,p52,p53]| = P
and A74:
for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
u)
= 0
by A39, A62;
( not
|[p51,p52,p53]| is
zero &
Dir |[p51,p52,p53]| = P )
by A73, A36, A38, EUCLID_5:3;
hence
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[p51,p52,p53]|)
= 0
by A74;
qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A75:
Dir |[p61,p62,p63]| = P
and A76:
for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
u)
= 0
by A43, A63;
( not
|[p61,p62,p63]| is
zero &
Dir |[p61,p62,p63]| = P )
by A75, A42, EUCLID_5:3, A40;
hence
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[p61,p62,p63]|)
= 0
by A76;
verum
end;
reconsider a2f = a2, b2f = b2, c2f = c2, d2f = d2, e2f = e2, f2f = f2 as Element of F_Real by XREAL_0:def 1;
( qfconic (a2f,b2f,c2f,d2f,e2,f2f,|[1,0,0]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[0,1,0]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[0,0,1]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[1,1,1]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[p51,p52,p53]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[p61,p62,p63]|) = 0 )
by A66;
then
( a2f = 0 & b2f = 0 & c2f = 0 )
by Th18;
then A77:
( a2f = 0 & b2f = 0 & c2f = 0 & (d2f + e2f) + f2f = 0 )
by A66, Th18;
reconsider r1 = d2, r2 = e2 as Real ;
reconsider p71 = p71, p72 = p72, p73 = p73, p81 = p81, p82 = p82, p83 = p83, p91 = p91, p92 = p92, p93 = p93 as Element of F_Real by XREAL_0:def 1;
( |[1,0,0]| = <*1,0,0*> & <*0,1,0*> = |[0,1,0]| & <*0,0,1*> = |[0,0,1]| & <*1,1,1*> = |[1,1,1]| & <*p51,p52,p53*> = |[p51,p52,p53]| & <*p61,p62,p63*> = |[p61,p62,p63]| & <*p71,p72,p73*> = |[p71,p72,p73]| & <*p81,p82,p83*> = |[p81,p82,p83]| & <*p91,p92,p93*> = |[p91,p92,p93]| )
;
then reconsider p1 = <*1,0,0*>, p2 = <*0,1,0*>, p3 = <*0,0,1*>, p4 = <*1,1,1*>, p5 = <*p51,p52,p53*>, p6 = <*p61,p62,p63*>, p7 = <*p71,p72,p73*>, p8 = <*p81,p82,p83*>, p9 = <*p91,p92,p93*> as Point of (TOP-REAL 3) ;
A82:
u5 = |[p51,p52,p53]|
by EUCLID_5:3, A38;
A83:
u6 = |[p61,p62,p63]|
by A42, EUCLID_5:3;
A84:
not p7 is zero
by A44, A46, EUCLID_5:3;
A85:
not p8 is zero
by A48, A50, EUCLID_5:3;
A86:
not p9 is zero
by A52, A54, EUCLID_5:3;
A87:
( ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 )
by A77, A66, A57;
A88:
|{p7,p2,p5}| <> 0
proof
A89:
not
(homography N) . P7,
(homography N) . P2,
(homography N) . P5 are_collinear
by A7, ANPROJ_8:102;
(
(homography N) . P7 = Dir p7 &
(homography N) . P2 = Dir p2 &
(homography N) . P5 = Dir p5 )
by A33, A38, A37, EUCLID_5:3, A45, A46;
hence
|{p7,p2,p5}| <> 0
by ANPROJ_8:43, A89, A84, ANPROJ_9:10, A82, A36, ANPROJ_2:23;
verum
end;
A90:
( p51 is Element of F_Real & p52 is Element of F_Real & p53 is Element of F_Real & p61 is Element of F_Real & p62 is Element of F_Real & p63 is Element of F_Real )
by XREAL_0:def 1;
now ( |{p1,p2,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )thus
|{p1,p2,p5}| <> 0
( |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P1,
(homography N) . P2,
(homography N) . P5 are_collinear
by A8, ANPROJ_8:102;
hence
|{p1,p2,p5}| <> 0
by A32, A33, A37, ANPROJ_8:43, ANPROJ_9:10, A82, A36, ANPROJ_2:23;
verum
end; thus
|{p1,p2,p6}| <> 0
( |{p1,p3,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P1,
(homography N) . P2,
(homography N) . P6 are_collinear
by A9, ANPROJ_8:102;
hence
|{p1,p2,p6}| <> 0
by A32, A33, A41, ANPROJ_8:43, A83, A40, ANPROJ_9:10, ANPROJ_2:23;
verum
end; thus
|{p1,p3,p5}| <> 0
( |{p1,p3,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P1,
(homography N) . P3,
(homography N) . P5 are_collinear
by A10, ANPROJ_8:102;
hence
|{p1,p3,p5}| <> 0
by A34, A32, A37, ANPROJ_8:43, ANPROJ_9:10, A82, A36, ANPROJ_2:23;
verum
end; thus
|{p1,p3,p6}| <> 0
( |{p1,p5,p7}| <> 0 & |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P1,
(homography N) . P3,
(homography N) . P6 are_collinear
by A11, ANPROJ_8:102;
hence
|{p1,p3,p6}| <> 0
by A32, A41, A34, ANPROJ_8:43, A83, A40, ANPROJ_9:10, ANPROJ_2:23;
verum
end; thus
|{p1,p5,p7}| <> 0
( |{p2,p4,p5}| <> 0 & |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P1,
(homography N) . P5,
(homography N) . P7 are_collinear
by A12, ANPROJ_8:102;
hence
|{p1,p5,p7}| <> 0
by A32, A37, A47, ANPROJ_8:43, ANPROJ_9:10, A82, A36, A84, ANPROJ_2:23;
verum
end; thus
|{p2,p4,p5}| <> 0
( |{p2,p4,p6}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P2,
(homography N) . P4,
(homography N) . P5 are_collinear
by A13, ANPROJ_8:102;
hence
|{p2,p4,p5}| <> 0
by A33, A37, A35, ANPROJ_8:43, ANPROJ_9:10, A82, A36, ANPROJ_2:23;
verum
end; thus
|{p2,p4,p6}| <> 0
( |{p2,p4,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P2,
(homography N) . P4,
(homography N) . P6 are_collinear
by A14, ANPROJ_8:102;
hence
|{p2,p4,p6}| <> 0
by A33, A41, A35, ANPROJ_8:43, ANPROJ_9:10, A83, A40, ANPROJ_2:23;
verum
end; thus
|{p2,p4,p7}| <> 0
( |{p2,p5,p9}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P2,
(homography N) . P4,
(homography N) . P7 are_collinear
by A15, ANPROJ_8:102;
hence
|{p2,p4,p7}| <> 0
by A33, A47, A35, ANPROJ_8:43, ANPROJ_9:10, A84, ANPROJ_2:23;
verum
end; thus
|{p2,p5,p9}| <> 0
( |{p2,p6,p8}| <> 0 & |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P2,
(homography N) . P5,
(homography N) . P9 are_collinear
by A16, ANPROJ_8:102;
hence
|{p2,p5,p9}| <> 0
by A33, A37, A55, ANPROJ_8:43, ANPROJ_9:10, A82, A36, A86, ANPROJ_2:23;
verum
end; thus
|{p2,p6,p8}| <> 0
( |{p2,p8,p7}| <> 0 & |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P2,
(homography N) . P6,
(homography N) . P8 are_collinear
by A17, ANPROJ_8:102;
hence
|{p2,p6,p8}| <> 0
by A33, A41, A51, ANPROJ_8:43, ANPROJ_9:10, A83, A40, A85, ANPROJ_2:23;
verum
end; thus
|{p2,p8,p7}| <> 0
( |{p2,p9,p7}| <> 0 & |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
A91:
|{p2,p8,p7}| = - |{p2,p7,p8}|
by ANPROJ_8:29;
not
(homography N) . P2,
(homography N) . P7,
(homography N) . P8 are_collinear
by A18, ANPROJ_8:102;
hence
|{p2,p8,p7}| <> 0
by A33, A47, A51, A91, ANPROJ_8:43, ANPROJ_9:10, A84, A85, ANPROJ_2:23;
verum
end; thus
|{p2,p9,p7}| <> 0
( |{p3,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
A92:
|{p2,p9,p7}| = - |{p2,p7,p9}|
by ANPROJ_8:29;
not
(homography N) . P2,
(homography N) . P7,
(homography N) . P9 are_collinear
by A19, ANPROJ_8:102;
hence
|{p2,p9,p7}| <> 0
by A92, ANPROJ_8:43, A33, A47, A55, ANPROJ_9:10, A84, A86, ANPROJ_2:23;
verum
end; thus
|{p3,p4,p5}| <> 0
( |{p3,p4,p6}| <> 0 & |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P3,
(homography N) . P4,
(homography N) . P5 are_collinear
by A20, ANPROJ_8:102;
hence
|{p3,p4,p5}| <> 0
by A34, A35, A37, ANPROJ_8:43, ANPROJ_9:10, A82, A36, ANPROJ_2:23;
verum
end; thus
|{p3,p4,p6}| <> 0
( |{p3,p5,p8}| <> 0 & |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P3,
(homography N) . P4,
(homography N) . P6 are_collinear
by A21, ANPROJ_8:102;
hence
|{p3,p4,p6}| <> 0
by A34, A35, A41, ANPROJ_8:43, ANPROJ_9:10, A83, A40, ANPROJ_2:23;
verum
end; thus
|{p3,p5,p8}| <> 0
( |{p3,p6,p8}| <> 0 & |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P3,
(homography N) . P5,
(homography N) . P8 are_collinear
by A22, ANPROJ_8:102;
hence
|{p3,p5,p8}| <> 0
by A34, A37, A51, ANPROJ_8:43, ANPROJ_9:10, A82, A36, A85, ANPROJ_2:23;
verum
end; thus
|{p3,p6,p8}| <> 0
( |{p5,p7,p8}| <> 0 & |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P3,
(homography N) . P6,
(homography N) . P8 are_collinear
by A23, ANPROJ_8:102;
hence
|{p3,p6,p8}| <> 0
by ANPROJ_8:43, A34, A41, A51, ANPROJ_9:10, A83, A40, A85, ANPROJ_2:23;
verum
end; A93:
|{p5,p8,p7}| = - |{p5,p7,p8}|
by ANPROJ_8:29;
thus
|{p5,p7,p8}| <> 0
( |{p5,p8,p7}| <> 0 & |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
not
(homography N) . P5,
(homography N) . P7,
(homography N) . P8 are_collinear
by A24, ANPROJ_8:102;
hence
|{p5,p7,p8}| <> 0
by ANPROJ_8:43, A37, A47, A51, A82, A36, A84, A85, ANPROJ_2:23;
verum
end; hence
|{p5,p8,p7}| <> 0
by A93;
( |{p5,p9,p7}| <> 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )A94:
|{p5,p9,p7}| = - |{p5,p7,p9}|
by ANPROJ_8:29;
|{p5,p7,p9}| <> 0
proof
not
(homography N) . P5,
(homography N) . P7,
(homography N) . P9 are_collinear
by A25, ANPROJ_8:102;
hence
|{p5,p7,p9}| <> 0
by A37, A47, A55, ANPROJ_8:43, A82, A36, A84, A86, ANPROJ_2:23;
verum
end; hence
|{p5,p9,p7}| <> 0
by A94;
( |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )thus
(
|{p1,p5,p9}| = 0 &
|{p1,p6,p8}| = 0 &
|{p2,p4,p9}| = 0 &
|{p2,p6,p7}| = 0 &
|{p3,p4,p8}| = 0 &
|{p3,p5,p7}| = 0 )
verumproof
thus
|{p1,p5,p9}| = 0
( |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A95:
(homography N) . P1 = Dir u
and A96:
(homography N) . P5 = Dir v
and A97:
(homography N) . P9 = Dir w
and A98:
not
u is
zero
and A99:
not
v is
zero
and A100:
not
w is
zero
and A101:
u,
v,
w are_LinDep
by A26, ANPROJ_8:102, ANPROJ_2:23;
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A98, A99, A100, A101, ANPROJ_1:25;
then
p1,
p5,
p9 are_LinDep
by A32, A37, A55, A95, A96, A97, ANPROJ_9:10, A82, A36, A86, ANPROJ_1:25;
hence
|{p1,p5,p9}| = 0
by ANPROJ_8:43;
verum
end;
thus
|{p1,p6,p8}| = 0
( |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A102:
(homography N) . P1 = Dir u
and A103:
(homography N) . P6 = Dir v
and A104:
(homography N) . P8 = Dir w
and A105:
not
u is
zero
and A106:
not
v is
zero
and A107:
not
w is
zero
and A108:
u,
v,
w are_LinDep
by A27, ANPROJ_8:102, ANPROJ_2:23;
A109:
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A105, A106, A107, A108, ANPROJ_1:25;
p1,
p6,
p8 are_LinDep
by A32, A41, A51, A102, A103, A104, A109, ANPROJ_9:10, A83, A40, A85, ANPROJ_1:25;
hence
|{p1,p6,p8}| = 0
by ANPROJ_8:43;
verum
end;
thus
|{p2,p4,p9}| = 0
( |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A110:
(homography N) . P2 = Dir u
and A111:
(homography N) . P4 = Dir v
and A112:
(homography N) . P9 = Dir w
and A113:
not
u is
zero
and A114:
not
v is
zero
and A115:
not
w is
zero
and A116:
u,
v,
w are_LinDep
by A28, ANPROJ_8:102, ANPROJ_2:23;
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A113, A114, A115, A116, ANPROJ_1:25;
then
p2,
p4,
p9 are_LinDep
by A33, A35, A55, A110, A111, A112, ANPROJ_9:10, A86, ANPROJ_1:25;
hence
|{p2,p4,p9}| = 0
by ANPROJ_8:43;
verum
end;
thus
|{p2,p6,p7}| = 0
( |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 )proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A117:
(homography N) . P2 = Dir u
and A118:
(homography N) . P6 = Dir v
and A119:
(homography N) . P7 = Dir w
and A120:
not
u is
zero
and A121:
not
v is
zero
and A122:
not
w is
zero
and A123:
u,
v,
w are_LinDep
by A29, ANPROJ_8:102, ANPROJ_2:23;
A124:
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A120, A121, A122, A123, ANPROJ_1:25;
p2,
p6,
p7 are_LinDep
by A33, A41, A47, A117, A118, A119, A124, ANPROJ_9:10, A83, A40, A84, ANPROJ_1:25;
hence
|{p2,p6,p7}| = 0
by ANPROJ_8:43;
verum
end;
thus
|{p3,p4,p8}| = 0
|{p3,p5,p7}| = 0 proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A125:
(homography N) . P3 = Dir u
and A126:
(homography N) . P4 = Dir v
and A127:
(homography N) . P8 = Dir w
and A128:
not
u is
zero
and A129:
not
v is
zero
and A130:
not
w is
zero
and A131:
u,
v,
w are_LinDep
by A30, ANPROJ_8:102, ANPROJ_2:23;
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A128, A129, A130, A131, ANPROJ_1:25;
then
p3,
p4,
p8 are_LinDep
by A34, A35, A51, A125, A126, A127, ANPROJ_9:10, A85, ANPROJ_1:25;
hence
|{p3,p4,p8}| = 0
by ANPROJ_8:43;
verum
end;
thus
|{p3,p5,p7}| = 0
verumproof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A132:
(homography N) . P3 = Dir u
and A133:
(homography N) . P5 = Dir v
and A134:
(homography N) . P7 = Dir w
and A135:
not
u is
zero
and A136:
not
v is
zero
and A137:
not
w is
zero
and A138:
u,
v,
w are_LinDep
by A31, ANPROJ_8:102, ANPROJ_2:23;
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A135, A136, A137, A138, ANPROJ_1:25;
then
p3,
p5,
p7 are_LinDep
by A34, A37, A47, A132, A133, A134, ANPROJ_9:10, A82, A36, A84, ANPROJ_1:25;
hence
|{p3,p5,p7}| = 0
by ANPROJ_8:43;
verum
end;
end; end;
then
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
by A90, A87, Th29;
then
|{p7,p2,p5}| * |{p7,p8,p9}| = 0
by Th30;
then
|{p7,p8,p9}| = 0
by A88, XCMPLX_1:6;
then A139:
p7,p8,p9 are_LinDep
by ANPROJ_8:43;
( (homography N) . P7 = Dir p7 & (homography N) . P8 = Dir p8 & (homography N) . P9 = Dir p9 & not p7 is zero & not p8 is zero & not p9 is zero )
by A52, A54, EUCLID_5:3, A44, A46, A50, A48, A45, A49, A53;
hence
P7,P8,P9 are_collinear
by A139, ANPROJ_2:23, ANPROJ_8:102; verum