:: Hessenberg Theorem
:: by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received October 2, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: HESSENBE:1

for PCPP being CollProjectiveSpace
for a, b, c being Element of PCPP st a,b,c are_collinear holds
( b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear )

proof end;

theorem Th2: :: HESSENBE:2

for PCPP being CollProjectiveSpace
for a, b, c, d being Element of PCPP st a <> b & a,b,c are_collinear & a,b,d are_collinear holds
a,c,d are_collinear

proof end;

theorem :: HESSENBE:3

for PCPP being CollProjectiveSpace
for a, b, p, r, q being Element of PCPP st p <> q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear holds
a,b,r are_collinear

proof end;

theorem Th4: :: HESSENBE:4

for PCPP being CollProjectiveSpace
for p, q being Element of PCPP st p <> q holds
ex r being Element of PCPP st not p,q,r are_collinear

proof end;

theorem :: HESSENBE:5

for PCPP being CollProjectiveSpace
for p being Element of PCPP holds
not for q, r being Element of PCPP holds p,q,r are_collinear

proof end;

theorem Th6: :: HESSENBE:6

for PCPP being CollProjectiveSpace
for a, b, b9, c being Element of PCPP st not a,b,c are_collinear & a,b,b9 are_collinear & a <> b9 holds
not a,b9,c are_collinear

proof end;

theorem Th7: :: HESSENBE:7

for PCPP being CollProjectiveSpace
for a, b, c, d being Element of PCPP st not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear holds
a = d

proof end;

theorem Th8: :: HESSENBE:8

for PCPP being CollProjectiveSpace
for a, a9, d, d9, o, x being Element of PCPP st not o,a,d are_collinear & o,d,d9 are_collinear & d <> d9 & a9,d9,x are_collinear & o,a,a9 are_collinear & o <> a9 holds
x <> d

proof end;

theorem Th9: :: HESSENBE:9

for PCPP being CollProjectiveSpace
for a1, a2, a3, c1, c3, x being Element of PCPP st not a1,a2,a3 are_collinear & a1,a2,c3 are_collinear & a2,a3,c1 are_collinear & c1,c3,x are_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds
( a1 <> x & a3 <> x )

proof end;

theorem Th10: :: HESSENBE:10

for PCPP being CollProjectiveSpace
for a, b, c, d, e being Element of PCPP st not a,b,c are_collinear & a,b,d are_collinear & c,e,d are_collinear & e <> c & d <> a holds
not e,a,c are_collinear

proof end;

theorem Th11: :: HESSENBE:11

for PCPP being CollProjectiveSpace
for p1, p2, q1, q2, q3 being Element of PCPP st not p1,p2,q1 are_collinear & p1,p2,q2 are_collinear & q1,q2,q3 are_collinear & q2 <> q3 holds
not p2,p1,q3 are_collinear

proof end;

theorem :: HESSENBE:12

for PCPP being CollProjectiveSpace
for p1, p2, p3, q1, q2 being Element of PCPP st not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p3 are_collinear & p3 <> q2 & p2 <> p3 holds
not p3,p2,q2 are_collinear

proof end;

theorem Th13: :: HESSENBE:13

for PCPP being CollProjectiveSpace
for p1, p2, p3, q1, q2 being Element of PCPP st not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p1 are_collinear & p1 <> p3 & p1 <> q2 holds
not p3,p1,q2 are_collinear

proof end;

theorem Th14: :: HESSENBE:14

for PCPP being CollProjectiveSpace
for a1, a2, b1, b2, x, y being Element of PCPP st a1 <> a2 & b1 <> b2 & b1,b2,x are_collinear & b1,b2,y are_collinear & a1,a2,x are_collinear & a1,a2,y are_collinear & not a1,a2,b1 are_collinear holds
x = y

proof end;

theorem Th15: :: HESSENBE:15

for PCPP being CollProjectiveSpace
for a1, a2, b1, b2, o being Element of PCPP st not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o <> b1 & o <> b2 holds
not o,b1,b2 are_collinear

proof end;

theorem Th16: :: HESSENBE:16

for PCPP being Pappian CollProjectivePlane
for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of PCPP st 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 holds
r1,r2,r3 are_collinear

proof end;

Lm1: for PCPP being Pappian CollProjectivePlane
for a1, a2, a3, b1, b2, b3, c1, c2, c3, o being Element of PCPP st o <> b1 & o <> b2 & not o,a1,a2 are_collinear & not o,a1,a3 are_collinear & not o,a2,a3 are_collinear & a1,a2,c3 are_collinear & b1,b2,c3 are_collinear & a2,a3,c1 are_collinear & b2,b3,c1 are_collinear & a1,a3,c2 are_collinear & b1,b3,c2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o,a3,b3 are_collinear & ( a1,a2,a3 are_collinear or b1,b2,b3 are_collinear ) holds
c1,c2,c3 are_collinear

proof end;

Lm2: for PCPP being Pappian CollProjectivePlane
for a1, a2, a3, b1, b2, b3, c1, c2, c3, o, x being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 are_collinear & not o,a1,a3 are_collinear & not o,a2,a3 are_collinear & not o,c1,c3 are_collinear & a1,a2,c3 are_collinear & b1,b2,c3 are_collinear & a2,a3,c1 are_collinear & b2,b3,c1 are_collinear & a1,a3,c2 are_collinear & b1,b3,c2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o,a3,b3 are_collinear & o,a2,x are_collinear & a1,a3,x are_collinear & not c1,c3,x are_collinear holds
c1,c2,c3 are_collinear

proof end;

Lm3: for PCPP being Pappian CollProjectivePlane
for a1, a2, a3, b1, b2, b3, c1, c2, c3, o being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 are_collinear & not o,a1,a3 are_collinear & not o,a2,a3 are_collinear & not o,c1,c3 are_collinear & a1,a2,c3 are_collinear & b1,b2,c3 are_collinear & a2,a3,c1 are_collinear & b2,b3,c1 are_collinear & a1,a3,c2 are_collinear & b1,b3,c2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o,a3,b3 are_collinear holds
c1,c2,c3 are_collinear

proof end;

theorem Th17: :: HESSENBE:17

for PCPP being Pappian CollProjectivePlane
for a1, a2, a3, b1, b2, b3, c1, c2, c3, o being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 are_collinear & not o,a1,a3 are_collinear & not o,a2,a3 are_collinear & a1,a2,c3 are_collinear & b1,b2,c3 are_collinear & a2,a3,c1 are_collinear & b2,b3,c1 are_collinear & a1,a3,c2 are_collinear & b1,b3,c2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o,a3,b3 are_collinear holds
c1,c2,c3 are_collinear

proof end;

registration

cluster V40() V104() V105() proper Vebleian at_least_3rank Pappian -> Desarguesian for L13();

coherence
for b₁ being CollProjectiveSpace st b₁ is Pappian holds
b₁ is Desarguesian

proof end;

end;