PAPPUS: Pappus's Hexagon Theorem in Real Projective Plane

:: Pappus's Hexagon Theorem in Real Projective Plane
:: by Roland Coghetto
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

theorem Th1: :: PAPPUS:1

for a, b, c, d, e, f, g, h, i being Real
for M being Matrix of 3,REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)

proof end;

Lm1: for b, c, d, e, f, g, h, i being Real
for M being Matrix of 3,REAL st M = <*<*0,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = (((- ((c * e) * g)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)

proof end;

Lm2: for b, d, e, f, g, h, i being Real
for M being Matrix of 3,REAL st M = <*<*0,b,0*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((b * f) * g) - ((b * d) * i)

proof end;

Lm3: for b, e, f, g, h, i being Real
for M being Matrix of 3,REAL st M = <*<*0,b,0*>,<*0,e,f*>,<*g,h,i*>*> holds
Det M = (b * f) * g

proof end;

Lm4: for a, d, e, f, h, i being Real
for M being Matrix of 3,REAL st M = <*<*a,0,0*>,<*d,e,f*>,<*0,h,i*>*> holds
Det M = ((a * e) * i) - ((a * h) * f)

proof end;

theorem Th2: :: PAPPUS:2

for P1, P4, P5 being Element of (ProjectiveSpace (TOP-REAL 3))
for p1, p2, p3, p4, p5 being Element of (TOP-REAL 3) st not p1 is zero & P1 = Dir p1 & not p4 is zero & P4 = Dir p4 & not p5 is zero & P5 = Dir p5 & P1,P4,P5 are_collinear holds
|{p1,p2,p4}| * |{p1,p3,p5}| = |{p1,p2,p5}| * |{p1,p3,p4}|

proof end;

theorem Th3: :: PAPPUS:3

for r416, r415, r413, r418, r419, r412, r712, r746, r716, r742, r715, r743, r713, r745, r749, r718, r719, r748 being non zero Real st (- r412) * (- r713) = (- r413) * (- r712) & (- r415) * (- r719) = (- r419) * (- r715) & (- r418) * (- r716) = (- r416) * (- r718) & (- r745) * r416 = (- r746) * r415 & (- r748) * r413 = (- r743) * r418 & (- r742) * r419 = (- r749) * r412 & r712 * r746 = r716 * r742 & r715 * r743 = r713 * r745 holds
r718 * r749 = r719 * r748

proof end;

theorem Th4: :: PAPPUS:4

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & c7 <> c6 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( not c4,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear )

proof end;

theorem Th5: :: PAPPUS:5

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c10 being Element of PCPP st not c2 = c1 & not c3 = c2 & not c5 = c1 & not c7 = c5 & not c7 = c6 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
not c10,c7,c8 are_collinear

proof end;

theorem Th6: :: PAPPUS:6

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( c4,c2,c3 are_collinear & c4,c5,c8 are_collinear & c4,c9,c6 are_collinear & c7,c5,c6 are_collinear & c7,c9,c3 are_collinear & c7,c2,c8 are_collinear & c10,c2,c6 are_collinear & c10,c5,c3 are_collinear )

proof end;

theorem Th7: :: PAPPUS:7

for PCPP being CollProjectiveSpace
for c1, c2, c3, c5, c6 being Element of PCPP st c3 <> c1 & c3 <> c2 & c6 <> c1 & c6 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c5,c6 are_collinear holds
( not c2,c3,c5 are_collinear & not c2,c3,c6 are_collinear & not c2,c5,c6 are_collinear & not c3,c5,c6 are_collinear )

proof end;

theorem Th8: :: PAPPUS:8

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7 being Element of PCPP st c3 <> c1 & c4 <> c1 & c4 <> c3 & c3 <> c2 & c4 <> c2 & c6 <> c1 & c7 <> c1 & c7 <> c6 & c6 <> c5 & c7 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
( not c1,c3,c6 are_collinear & c1,c3,c4 are_collinear & c1,c6,c7 are_collinear & c3 <> c1 & c2 <> c1 & c3 <> c2 & c4 <> c3 & c4 <> c2 & c6 <> c1 & c5 <> c1 & c6 <> c5 & c7 <> c6 & c7 <> c5 & not c1,c4,c7 are_collinear & c1,c4,c3 are_collinear & c1,c4,c2 are_collinear & c1,c7,c6 are_collinear & c1,c7,c5 are_collinear )

proof end;

theorem Th9: :: PAPPUS:9

for PCPP being CollProjectiveSpace
for c2, c3, c4, c6, c8 being Element of PCPP st c4 <> c2 & c4 <> c3 & c8 <> c2 & not c2,c3,c6 are_collinear & c2,c3,c4 are_collinear & c2,c6,c8 are_collinear holds
not c3,c4,c8 are_collinear

proof end;

theorem Th10: :: PAPPUS:10

for PCPP being CollProjectiveSpace
for c1, c2, c4, c5, c6, c8 being Element of PCPP st c4 <> c1 & c6 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear holds
c8 <> c5

proof end;

theorem Th11: :: PAPPUS:11

for PCPP being CollProjectiveSpace
for c1, c2, c4, c5, c6, c8 being Element of PCPP st c4 <> c2 & c6 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear holds
c8 <> c2

proof end;

theorem Th12: :: PAPPUS:12

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear holds
c2,c3,c4 are_collinear

proof end;

theorem Th13: :: PAPPUS:13

for PCPP being CollProjectiveSpace
for c1, c2, c5, c6, c7 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
c5,c6,c7 are_collinear

proof end;

theorem Th14: :: PAPPUS:14

for PCPP being CollProjectiveSpace
for c1, c2, c3, c5, c7 being Element of PCPP st c3 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c5,c7 are_collinear holds
c7 <> c3

proof end;

theorem Th15: :: PAPPUS:15

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c9 being Element of PCPP st c4 <> c1 & c4 <> c3 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear & c4,c5,c9 are_collinear holds
c9 <> c3

proof end;

theorem Th16: :: PAPPUS:16

for PCPP being CollProjectiveSpace
for c1, c2, c4, c5, c6, c7, c9 being Element of PCPP st c4 <> c1 & c4 <> c2 & c6 <> c1 & c7 <> c6 & c7 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear & c2,c7,c9 are_collinear & c4,c5,c9 are_collinear holds
not c9,c2,c5 are_collinear

proof end;

Lm5: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 & not p1,q1,r1 are_collinear holds
r1,r2,r3 are_collinear

proof end;

Lm6: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 & p1,q1,r1 are_collinear & p2,q2,r2 are_collinear & p3,q3,r3 are_collinear holds
r1,r2,r3 are_collinear

proof end;

Lm7: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 & p1,q1,r1 are_collinear holds
r1,r2,r3 are_collinear

proof end;

::

WP:

theorem :: PAPPUS:17

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 holds
r1,r2,r3 are_collinear

proof end;

theorem :: PAPPUS:18

ProjectiveSpace (TOP-REAL 3) is Desarguesian Pappian CollProjectivePlane by ANPROJ_8:57;

theorem Th19: :: PAPPUS:19

for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of (ProjectiveSpace (TOP-REAL 3)) st c1 <> c2 & c1 <> c3 & c2 <> c3 & c2 <> c4 & c3 <> c4 & c1 <> c5 & c1 <> c6 & c5 <> c6 & c5 <> c7 & c6 <> c7 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( not c4,c2,c7 are_collinear & not c4,c3,c7 are_collinear & not c2,c3,c7 are_collinear & not c4,c2,c5 are_collinear & not c4,c2,c6 are_collinear & not c4,c3,c5 are_collinear & not c4,c3,c6 are_collinear & not c2,c7,c5 are_collinear & not c2,c7,c6 are_collinear & not c3,c7,c5 are_collinear & not c3,c7,c6 are_collinear & not c2,c3,c5 are_collinear & not c2,c3,c6 are_collinear & not c7,c5,c4 are_collinear & not c7,c6,c4 are_collinear & not c5,c6,c4 are_collinear & not c5,c6,c2 are_collinear & c4,c5,c8 are_collinear & c4,c6,c9 are_collinear & c2,c7,c8 are_collinear & c2,c6,c10 are_collinear & c3,c7,c9 are_collinear & c3,c5,c10 are_collinear )

proof end;

theorem :: PAPPUS:20

conic (0,0,0,0,0,0) = the carrier of (ProjectiveSpace (TOP-REAL 3))

proof end;

theorem :: PAPPUS:21

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 holds
p1,p2,p3,q1,q2,q3,r1,r2,r3 are_in_Pascal_configuration by Th19;

::

WP:

theorem :: PAPPUS:22

for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of (ProjectiveSpace (TOP-REAL 3)) st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,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 holds
r1,r2,r3 are_collinear

proof end;