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) & P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration 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) & P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration 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:
P1,P2,P3 are_collinear
and
A4:
P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration
; P7,P8,P9 are_collinear
not P1,P4,P5 are_collinear
by A4, COLLSP:8;
then consider N being invertible Matrix of 3,F_Real such that
A5:
(homography N) . P1 = Dir100
and
A6:
(homography N) . P2 = Dir010
and
A7:
(homography N) . P4 = Dir001
and
A8:
(homography N) . P5 = Dir111
by A4, ANPROJ_9:30;
consider u3 being Point of (TOP-REAL 3) such that
A9:
not u3 is zero
and
A10:
(homography N) . P3 = Dir u3
by ANPROJ_1:26;
reconsider p31 = u3 . 1, p32 = u3 . 2, p33 = u3 . 3 as Real ;
A11:
( u3 `1 = u3 . 1 & u3 `2 = u3 . 2 & u3 `3 = u3 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A12:
(homography N) . P3 = Dir |[p31,p32,p33]|
by A10, EUCLID_5:3;
consider u6 being Point of (TOP-REAL 3) such that
A13:
not u6 is zero
and
A14:
(homography N) . P6 = Dir u6
by ANPROJ_1:26;
reconsider p61 = u6 . 1, p62 = u6 . 2, p63 = u6 . 3 as Real ;
A15:
( 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 A16:
(homography N) . P6 = Dir |[p61,p62,p63]|
by A14, EUCLID_5:3;
A17:
( 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
A18:
( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 )
and
A19:
(homography N) . P1 in conic (a2,b2,c2,d2,e2,f2)
and
A20:
(homography N) . P2 in conic (a2,b2,c2,d2,e2,f2)
and
A21:
(homography N) . P3 in conic (a2,b2,c2,d2,e2,f2)
and
A22:
(homography N) . P4 in conic (a2,b2,c2,d2,e2,f2)
and
A23:
(homography N) . P5 in conic (a2,b2,c2,d2,e2,f2)
and
A24:
(homography N) . P6 in conic (a2,b2,c2,d2,e2,f2)
by A17, A2, A1, Th17;
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A25:
Dir |[1,0,0]| = P
and
A26:
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 A5, A19;
A27:
( 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,|[p31,p32,p33]|) = 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 A25, A26, 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,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A28:
Dir |[0,1,0]| = P
and A29:
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 A6, A20;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[0,1,0]|)
= 0
by A28, A29, 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,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A30:
Dir |[0,0,1]| = P
and A31:
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 A7, A22;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[0,0,1]|)
= 0
by A30, A31, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A32:
Dir |[1,1,1]| = P
and A33:
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 A8, A23;
thus
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[1,1,1]|)
= 0
by A32, A33, ANPROJ_9:10;
( qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A34:
Dir |[p31,p32,p33]| = P
and A35:
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 A12, A21;
( not
|[p31,p32,p33]| is
zero &
Dir |[p31,p32,p33]| = P )
by A34, A9, A11, EUCLID_5:3;
hence
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[p31,p32,p33]|)
= 0
by A35;
qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0
consider P being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A36:
Dir |[p61,p62,p63]| = P
and A37:
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 A16, A24;
( not
|[p61,p62,p63]| is
zero &
Dir |[p61,p62,p63]| = P )
by A36, A15, EUCLID_5:3, A13;
hence
qfconic (
a2,
b2,
c2,
d2,
e2,
f2,
|[p61,p62,p63]|)
= 0
by A37;
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,|[p31,p32,p33]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[p61,p62,p63]|) = 0 )
by A27;
then A38:
( a2f = 0 & b2f = 0 & c2f = 0 )
by Th18;
then A39:
( a2f = 0 & b2f = 0 & c2f = 0 & (d2f + e2f) + f2f = 0 )
by A27, Th18;
reconsider r1 = d2, r2 = f2 as Real ;
( |[1,0,0]| = <*1,0,0*> & <*0,1,0*> = |[0,1,0]| & <*0,0,1*> = |[0,0,1]| & <*1,1,1*> = |[1,1,1]| & <*p31,p32,p33*> = |[p31,p32,p33]| & <*p61,p62,p63*> = |[p61,p62,p63]| )
;
then reconsider p1 = <*1,0,0*>, p2 = <*0,1,0*>, p4 = <*0,0,1*>, p5 = <*1,1,1*>, p3 = <*p31,p32,p33*>, p6 = <*p61,p62,p63*> as Point of (TOP-REAL 3) ;
A42:
u3 = |[p31,p32,p33]|
by EUCLID_5:3, A11;
A43:
u6 = |[p61,p62,p63]|
by A15, EUCLID_5:3;
A44:
( ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,(- (r1 + r2)),r2,p3) = 0 & qfconic (0,0,0,r1,(- (r1 + r2)),r2,p6) = 0 )
by A39, A27, A18;
A45:
( p1 `1 = 1 & p1 `2 = 0 & p1 `3 = 0 & p2 `1 = 0 & p2 `2 = 1 & p2 `3 = 0 & p3 `1 = p31 & p3 `2 = p32 & p3 `3 = p33 )
by EUCLID_5:2;
A46:
( p3 `1 = p3 . 1 & p3 `2 = p3 . 2 & p3 `3 = p3 . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A47:
( (homography N) . P1 = Dir p1 & (homography N) . P2 = Dir p2 & (homography N) . P3 = Dir p3 )
by A5, A6, A11, A10, EUCLID_5:3;
|{p1,p2,p3}| = 0
proof
consider u,
v,
w being
Element of
(TOP-REAL 3) such that A48:
(homography N) . P1 = Dir u
and A49:
(homography N) . P2 = Dir v
and A50:
(homography N) . P3 = Dir w
and A51:
not
u is
zero
and A52:
not
v is
zero
and A53:
not
w is
zero
and A54:
u,
v,
w are_LinDep
by A3, ANPROJ_8:102, ANPROJ_2:23;
A55:
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A51, A52, A53, A54, ANPROJ_1:25;
p1,
p2,
p3 are_LinDep
by A5, A6, A10, ANPROJ_9:10, A42, A9, A48, A49, A50, A55, ANPROJ_1:25;
hence
|{p1,p2,p3}| = 0
by ANPROJ_8:43;
verum
end;
then A56: 0 =
((((((1 * (p2 `2)) * (p3 `3)) - ((0 * (p2 `2)) * (p3 `1))) - ((1 * (p2 `3)) * (p3 `2))) + ((0 * (p2 `3)) * (p3 `1))) - ((0 * (p2 `1)) * (p3 `3))) + ((0 * (p2 `1)) * (p3 `2))
by A45, ANPROJ_8:27
.=
p3 `3
by A45
;
A57:
( p31 <> 0 & p32 <> 0 )
proof
assume
(
p31 = 0 or
p32 = 0 )
;
contradiction
per cases then
( p31 = 0 or p32 = 0 )
;
suppose
p31 = 0
;
contradictionthen A58:
p3 =
|[(p32 * 0),(p32 * 1),(p32 * 0)]|
by A56, EUCLID_5:2
.=
p32 * |[0,1,0]|
by EUCLID_5:8
;
now ( are_Prop p3,|[0,1,0]| & not p3 is zero & not |[0,1,0]| is zero )
p32 <> 0
hence
are_Prop p3,
|[0,1,0]|
by A58, ANPROJ_1:1;
( not p3 is zero & not |[0,1,0]| is zero )thus
not
p3 is
zero
by A11, EUCLID_5:3, A9;
not |[0,1,0]| is zero thus
not
|[0,1,0]| is
zero
by ANPROJ_9:11;
verum end; then
(homography N) . P3 = (homography N) . P2
by A47, ANPROJ_1:22;
then
P3 = P2
by ANPROJ_9:16;
hence
contradiction
by A4, ANPROJ_2:def 7;
verum end; suppose
p32 = 0
;
contradictionthen A59:
p3 =
|[(p31 * 1),(p31 * 0),(p31 * 0)]|
by A56, EUCLID_5:2
.=
p31 * |[1,0,0]|
by EUCLID_5:8
;
now ( are_Prop p3,|[1,0,0]| & not p3 is zero & not |[1,0,0]| is zero )
p31 <> 0
hence
are_Prop p3,
|[1,0,0]|
by A59, ANPROJ_1:1;
( not p3 is zero & not |[1,0,0]| is zero )thus
not
p3 is
zero
by EUCLID_5:3, A11, A9;
not |[1,0,0]| is zero thus
not
|[1,0,0]| is
zero
by ANPROJ_9:11;
verum end; then
Dir p3 = Dir100
by ANPROJ_1:22;
then
P3 = P1
by A47, ANPROJ_9:16;
hence
contradiction
by ANPROJ_2:def 7, A4;
verum end; end;
end;
then
( r2 <> 0 & ( r2 * (p6 . 3) = 0 or (p6 . 1) - (p6 . 2) = 0 ) )
by XCMPLX_1:6;
per cases then
( p6 . 3 = 0 or p6 . 1 = p6 . 2 )
by XCMPLX_1:6;
suppose
p6 . 3
= 0
;
P7,P8,P9 are_collinear then A63:
p6 `3 = 0
by EUCLID_5:def 3;
A64:
p6 =
|[(p61 + 0),(0 + p62),(0 + 0)]|
by A63, EUCLID_5:2
.=
|[(p61 * 1),(p61 * 0),(p61 * 0)]| + |[(p62 * 0),(p62 * 1),(p62 * 0)]|
by EUCLID_5:6
.=
(p61 * |[1,0,0]|) + |[(p62 * 0),(p62 * 1),(p62 * 0)]|
by EUCLID_5:8
.=
(p61 * |[1,0,0]|) + (p62 * |[0,1,0]|)
by EUCLID_5:8
;
per cases
( ( p61 = 0 & p62 = 0 ) or ( p61 <> 0 & p62 = 0 ) or ( p61 = 0 & p62 <> 0 ) or ( p61 <> 0 & p62 <> 0 ) )
;
suppose A65:
(
p61 <> 0 &
p62 = 0 )
;
P7,P8,P9 are_collinear now ( are_Prop p6,|[1,0,0]| & not p6 is zero & not |[1,0,0]| is zero )p6 =
|[(p61 * 1),(p61 * 0),(p61 * 0)]|
by A63, EUCLID_5:2, A65
.=
p61 * |[1,0,0]|
by EUCLID_5:8
;
hence
are_Prop p6,
|[1,0,0]|
by A65, ANPROJ_1:1;
( not p6 is zero & not |[1,0,0]| is zero )thus
not
p6 is
zero
by A15, EUCLID_5:3, A13;
not |[1,0,0]| is zero thus
not
|[1,0,0]| is
zero
by ANPROJ_9:11;
verum end; then
Dir p6 = Dir100
by ANPROJ_1:22;
then
P1 = P6
by ANPROJ_9:16, A5, A14, A43;
hence
P7,
P8,
P9 are_collinear
by A4, ANPROJ_2:def 7;
verum end; suppose A66:
(
p61 = 0 &
p62 <> 0 )
;
P7,P8,P9 are_collinear now ( are_Prop p6,|[0,1,0]| & not p6 is zero & not |[0,1,0]| is zero )p6 =
|[(p62 * 0),(p62 * 1),(p62 * 0)]|
by A63, EUCLID_5:2, A66
.=
p62 * |[0,1,0]|
by EUCLID_5:8
;
hence
are_Prop p6,
|[0,1,0]|
by A66, ANPROJ_1:1;
( not p6 is zero & not |[0,1,0]| is zero )thus
not
p6 is
zero
by A15, EUCLID_5:3, A13;
not |[0,1,0]| is zero thus
not
|[0,1,0]| is
zero
by ANPROJ_9:11;
verum end; then
Dir p6 = Dir010
by ANPROJ_1:22;
then
P2 = P6
by ANPROJ_9:16, A6, A14, A43;
hence
P7,
P8,
P9 are_collinear
by A4, ANPROJ_2:def 7;
verum end; suppose
(
p61 <> 0 &
p62 <> 0 )
;
P7,P8,P9 are_collinear now ( |[1,0,0]|,|[0,1,0]|,p6 are_LinDep & not |[1,0,0]| is zero & not |[0,1,0]| is zero & not p6 is zero )now ( p6 = (p61 * |[1,0,0]|) + (p62 * |[0,1,0]|) & not |[1,0,0]| is zero & not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )thus
p6 = (p61 * |[1,0,0]|) + (p62 * |[0,1,0]|)
by A64;
( not |[1,0,0]| is zero & not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )thus
not
|[1,0,0]| is
zero
by ANPROJ_9:11;
( not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )thus
not
|[0,1,0]| is
zero
by ANPROJ_9:11;
not are_Prop |[1,0,0]|,|[0,1,0]|thus
not
are_Prop |[1,0,0]|,
|[0,1,0]|
verumproof
assume
are_Prop |[1,0,0]|,
|[0,1,0]|
;
contradiction
then consider a being
Real such that
a <> 0
and A67:
|[1,0,0]| = a * |[0,1,0]|
by ANPROJ_1:1;
|[1,0,0]| =
|[(a * 0),(a * 1),(a * 0)]|
by A67, EUCLID_5:8
.=
|[0,a,0]|
;
hence
contradiction
by FINSEQ_1:78;
verum
end; end; hence
|[1,0,0]|,
|[0,1,0]|,
p6 are_LinDep
by ANPROJ_1:6;
( not |[1,0,0]| is zero & not |[0,1,0]| is zero & not p6 is zero )thus
not
|[1,0,0]| is
zero
by ANPROJ_9:11;
( not |[0,1,0]| is zero & not p6 is zero )thus
not
|[0,1,0]| is
zero
by ANPROJ_9:11;
not p6 is zero thus
not
p6 is
zero
by A15, EUCLID_5:3, A13;
verum end; then
[Dir100,Dir010,(Dir p6)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by ANPROJ_1:25;
hence
P7,
P8,
P9 are_collinear
by A4, A5, A6, A14, A43, COLLSP:def 2, ANPROJ_8:102;
verum end; end; end; suppose A68:
p6 . 1
= p6 . 2
;
P7,P8,P9 are_collinear A69:
p61 =
p6 `1
by EUCLID_5:2
.=
p6 . 2
by A68, EUCLID_5:def 1
.=
p6 `2
by EUCLID_5:def 2
.=
p62
by EUCLID_5:2
;
now ( not p4 is zero & not p5 is zero & not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )thus
not
p4 is
zero
by ANPROJ_9:11;
( not p5 is zero & not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )thus
not
p5 is
zero
by ANPROJ_9:11;
( not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )thus
not
p6 is
zero
by A13, A15, EUCLID_5:3;
|[0,0,1]|,|[1,1,1]|,p6 are_LinDep
|{p4,p5,p6}| = 0
hence
|[0,0,1]|,
|[1,1,1]|,
p6 are_LinDep
by ANPROJ_8:43;
verum end; then A70:
[Dir001,Dir111,(Dir p6)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by ANPROJ_1:25;
reconsider p1 =
P1,
p2 =
P2,
p3 =
P3,
q1 =
P4,
q2 =
P5,
q3 =
P6,
r1 =
P7,
r2 =
P8,
r3 =
P9 as
Element of
(ProjectiveSpace (TOP-REAL 3)) ;
(
p2 <> p3 &
p1 <> p3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
p1,
p2,
q1 are_collinear &
p1,
p2,
p3 are_collinear &
q1,
q2,
q3 are_collinear &
p1,
q2,
r3 are_collinear &
q1,
p2,
r3 are_collinear &
p1,
q3,
r2 are_collinear &
p3,
q1,
r2 are_collinear &
p2,
q3,
r1 are_collinear &
p3,
q2,
r1 are_collinear )
by COLLSP:2, A3, A4, A70, A7, A8, A14, A43, COLLSP:def 2, ANPROJ_2:24, ANPROJ_8:102;
hence
P7,
P8,
P9 are_collinear
by ANPROJ_8:57, HESSENBE:16;
verum end; end;