:: Hessenberg Theorem
::  by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received October 2, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ANPROJ_2, SUBSET_1, AFF_2, INCSP_1, PENCIL_1;
 notations STRUCT_0, COLLSP, ANPROJ_2;
 constructors ANPROJ_2;
 registrations ANPROJ_2, PROJDES1;


begin

reserve PCPP for CollProjectiveSpace,
  a,a9,a1,a2,a3,b,b9,b1,b2,c,c1,c3,d,d9,e,
  o,p,p1,p2,p3,r,q, q1,q2,q3,x,y for Element of PCPP;

theorem :: HESSENBE:1
  a,b,c are_collinear implies 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;

theorem :: HESSENBE:2
  a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear;

theorem :: HESSENBE:3
  p<>q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear
  implies a,b,r are_collinear;

theorem :: HESSENBE:4
  p<>q implies ex r st not p,q,r are_collinear;

theorem :: HESSENBE:5
  ex q,r st not p,q,r are_collinear;

theorem :: HESSENBE:6
  not a,b,c are_collinear & a,b,b9 are_collinear & a<>b9 implies not
  a,b9,c are_collinear;

theorem :: HESSENBE:7
  not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear
implies a=d;

theorem :: HESSENBE:8
  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 implies x<>d;

theorem :: HESSENBE:9
  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
implies
  a1<>x & a3<>x;

theorem :: HESSENBE:10
  not a,b,c are_collinear & a,b,d are_collinear & c,e,d are_collinear
  & e<>c & d<>a implies not e,a,c are_collinear;

theorem :: HESSENBE:11
  not p1,p2,q1 are_collinear & p1,p2,q2 are_collinear & q1,q2,q3
  are_collinear & q2<>q3 implies not p2,p1,q3 are_collinear;

theorem :: HESSENBE:12
  not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p3
  are_collinear & p3<>q2 & p2<>p3 implies not p3,p2,q2 are_collinear;

theorem :: HESSENBE:13
  not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p1
  are_collinear & p1<>p3 & p1<>q2 implies not p3,p1,q2 are_collinear;

theorem :: HESSENBE:14
  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
implies
  x=y;

theorem :: HESSENBE:15
  not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2
  are_collinear & o<>b1 & o<>b2 implies not o,b1,b2 are_collinear;

reserve PCPP for Pappian CollProjectivePlane,
  a,a1,a2,a3,b1,b2,b3,c1,c2,c3,o,p
  ,p1,p2,p3,q,q9, q1,q2,q3,r,r1,r2,r3,x,y,z for Element of PCPP;

theorem :: HESSENBE:16
  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
implies r1,r2,r3
  are_collinear;

theorem :: HESSENBE:17
  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
implies c1,c2,c3
  are_collinear;

registration
  cluster Pappian -> Desarguesian for CollProjectiveSpace;
end;