:: The Collinearity Structure
::  by Wojciech Skaba
::
:: Received May 9, 1990
:: Copyright (c) 1990-2012 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 TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC,
      PARSP_2, RELAT_2, INCSP_1, NUMBERS, COLLSP;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, DOMAIN_1, STRUCT_0,
      PRE_TOPC;
 constructors DOMAIN_1, NUMBERS, STRUCT_0;
 registrations XBOOLE_0, ORDINAL1, STRUCT_0;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, STRUCT_0;
 theorems TARSKI, MCART_1, ENUMSET1, XBOOLE_0, XTUPLE_0;

begin :: AUXILIARY THEOREMS

reserve X for set;

definition
  let X;
  mode Relation3 of X -> set means
    :Def1:
    it c= [:X,X,X:];
  existence;
end;

theorem Th1:
  X = {} or ex a be set st {a} = X or ex a,b be set st a<>b & a in X & b in X
proof
  now
    set p = the Element of X;
    assume X <> {} & not ex a,b be set st a<>b & a in X & b in X;
    then for z be set holds z in X iff z = p;
    then X={p} by TARSKI:def 1;
    hence ex a be set st {a} = X;
  end;
  hence thesis;
end;

::                      *********************
::                      *   COLLINEARITY    *
::                      *********************

definition
  struct(1-sorted) CollStr (# carrier -> set, Collinearity -> Relation3 of the
    carrier #);
end;

registration
  cluster non empty strict for CollStr;
  existence
  proof
    set A = the non empty set,r = the Relation3 of A;
    take CollStr(#A,r#);
    thus the carrier of CollStr(#A,r#) is non empty;
    thus thesis;
  end;
end;

reserve CS for non empty CollStr;
reserve a,b,c for Point of CS;

definition
  let CS, a,b,c;
  pred a,b,c is_collinear means
  :Def2:
  [a,b,c] in the Collinearity of CS;
end;

set Z = {1};

Lm1: 1 in Z by TARSKI:def 1;

Lm2: {[1,1,1]} c= [:{1},{1},{1}:]
proof
  now
    let x be set;
    assume x in {[1,1,1]};
    then x = [1,1,1] by TARSKI:def 1;
    hence x in [:{1},{1},{1}:] by Lm1,MCART_1:69;
  end;
  hence thesis by TARSKI:def 3;
end;

reconsider Z as non empty set;
reconsider RR = {[1,1,1]} as Relation3 of Z by Def1,Lm2;
reconsider CLS = CollStr (# Z, RR #) as non empty CollStr;

Lm3: now
  let a,b,c,p,q,r be Point of CLS;
A1: for z1,z2,z3 being Point of CLS holds [z1,z2,z3] in the Collinearity of CLS
  proof
    let z1,z2,z3 be Point of CLS;
A2: z3 = 1 by TARSKI:def 1;
    z1 = 1 & z2 = 1 by TARSKI:def 1;
    hence thesis by A2,TARSKI:def 1;
  end;
  hence a=b or a=c or b=c implies [a,b,c] in the Collinearity of CLS;
  thus a<>b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity
of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity
  of CLS by A1;
end;

definition
  let IT be non empty CollStr;
  attr IT is reflexive means
  :Def3:
  for a,b,c being Point of IT st a=b or a=c
  or b=c holds [a,b,c] in the Collinearity of IT;
end;

definition
  let IT be non empty CollStr;
  attr IT is transitive means
  :Def4:
  for a,b,p,q,r being Point of IT st a<>b &
[a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r]
  in the Collinearity of IT holds [p,q,r] in the Collinearity of IT;
end;

registration
  cluster strict reflexive transitive for non empty CollStr;
  existence
  proof
    take CLS;
    thus thesis by Def3,Def4,Lm3;
  end;
end;

definition
  mode CollSp is reflexive transitive non empty CollStr;
end;

reserve CLSP for CollSp;
reserve a,b,c,d,p,q,r for Point of CLSP;

theorem Th2:
  (a=b or a=c or b=c) implies a,b,c is_collinear
proof
  assume a=b or a=c or b=c;
  then [a,b,c] in the Collinearity of CLSP by Def3;
  hence thesis by Def2;
end;

theorem Th3:
  a<>b & a,b,p is_collinear & a,b,q is_collinear & a,b,r
  is_collinear implies p,q,r is_collinear
proof
  assume that
A1: a<>b and
A2: a,b,p is_collinear & a,b,q is_collinear and
A3: a,b,r is_collinear;
A4: [a,b,r] in the Collinearity of CLSP by A3,Def2;
  [a,b,p] in the Collinearity of CLSP & [a,b,q] in the Collinearity of
  CLSP by A2,Def2;
  then [p,q,r] in the Collinearity of CLSP by A1,A4,Def4;
  hence thesis by Def2;
end;

theorem Th4:
  a,b,c is_collinear implies b,a,c is_collinear & a,c,b is_collinear
proof
  assume
A1: a,b,c is_collinear;
  then a=b or a<>b & a,b,b is_collinear & a,b,a is_collinear & a,b,c
  is_collinear by Th2;
  hence b,a,c is_collinear by Th2,Th3;
  a=b or a<>b & a,b,a is_collinear & a,b,c is_collinear & a,b,b
  is_collinear by A1,Th2;
  hence a,c,b is_collinear by Th2,Th3;
end;

theorem
  a,b,a is_collinear by Th2;

theorem Th6:
  a<>b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear
proof
  assume
A1: a<>b & a,b,c is_collinear & a,b,d is_collinear;
  a,b,a is_collinear by Th2;
  hence thesis by A1,Th3;
end;

theorem
  a,b,c is_collinear implies b,a,c is_collinear by Th4;

theorem Th8:
  a,b,c is_collinear implies b,c,a is_collinear
proof
  assume a,b,c is_collinear;
  then b,a,c is_collinear by Th4;
  hence thesis by Th4;
end;

theorem Th9:
  p<>q & a,b,p is_collinear & a,b,q is_collinear & p,q,r
  is_collinear implies a,b,r is_collinear
proof
  assume that
A1: p<>q and
A2: a,b,p is_collinear & a,b,q is_collinear and
A3: p,q,r is_collinear;
  now
    assume
A4: a<>b;
    then a,p,q is_collinear by A2,Th6;
    then
A5: p,q,a is_collinear by Th8;
    a,b,b is_collinear by Th2;
    then p,q,b is_collinear by A2,A4,Th3;
    hence thesis by A1,A3,A5,Th3;
  end;
  hence thesis by Th2;
end;

::                      *******************
::                      *      LINES      *
::                      *******************

definition
  let CLSP,a,b;
  func Line(a,b) -> set equals
  {p: a,b,p is_collinear};
  correctness;
end;

theorem Th10:
  a in Line(a,b) & b in Line(a,b)
proof
  a,b,a is_collinear by Th2;
  hence a in Line(a,b);
  a,b,b is_collinear by Th2;
  hence b in Line(a,b);
end;

theorem Th11:
  a,b,r is_collinear iff r in Line(a,b)
proof
  thus a,b,r is_collinear implies r in Line(a,b);
  thus r in Line(a,b) implies a,b,r is_collinear
  proof
    assume r in Line(a,b);
    then ex p st r=p & a,b,p is_collinear;
    hence thesis;
  end;
end;

::                ************************************
::                *    PROPER COLLINEARITY SPACES    *
::                ************************************

reserve i,j,k for Element of NAT;

set Z = {1, 2, 3};
set RR = { [i,j,k]: (i=j or j=k or k=i) & i in Z & j in Z & k in Z };

Lm4: RR c= [:Z,Z,Z:]
proof
  now
    let x be set;
    assume x in RR;
    then
    ex i,j,k st x = [i,j,k] & (i=j or j=k or k=i) & i in Z & j in Z & k in Z;
    hence x in [:Z,Z,Z:] by MCART_1:69;
  end;
  hence thesis by TARSKI:def 3;
end;

reconsider Z as non empty set by ENUMSET1:def 1;
reconsider RR as Relation3 of Z by Def1,Lm4;
reconsider CLS = CollStr (# Z, RR #) as non empty CollStr;

Lm5: for a,b,c be Point of CLS holds [a,b,c] in RR iff (a=b or b=c or c =a) &
a in Z & b in Z & c in Z
proof
  let a,b,c be Point of CLS;
  thus [a,b,c] in RR implies (a=b or b=c or c =a) & a in Z & b in Z & c in Z
  proof
    assume [a,b,c] in RR;
    then consider i,j,k such that
A1: [a,b,c] = [i,j,k] and
A2: i=j or j=k or k=i and
    i in Z and
    j in Z and
    k in Z;
    a=i & b=j by A1,XTUPLE_0:3;
    hence thesis by A1,A2,XTUPLE_0:3;
  end;
  thus thesis;
end;

Lm6: for a,b,c,p,q,r be Point of CLS holds (a<>b & [a,b,p] in the Collinearity
of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of
CLS implies [p,q,r] in the Collinearity of CLS)
proof
  let a,b,c,p,q,r be Point of CLS;
  assume that
A1: a<>b and
A2: [a,b,p] in the Collinearity of CLS and
A3: [a,b,q] in the Collinearity of CLS and
A4: [a,b,r] in the Collinearity of CLS;
A5: a=q or b=q by A1,A3,Lm5;
A6: a=r or b=r by A1,A4,Lm5;
A7: p in Z & q in Z;
A8: r in Z;
  a=p or b=p by A1,A2,Lm5;
  hence [p,q,r] in the Collinearity of CLS by A5,A6,A7,A8;
end;

Lm7: ex a,b,c be Point of CLS st not a,b,c is_collinear
proof
  reconsider a=1,b=2,c =3 as Point of CLS by ENUMSET1:def 1;
  take a,b,c;
  not [a,b,c] in the Collinearity of CLS by Lm5;
  hence thesis by Def2;
end;

Lm8: CLS is CollSp
proof
  for a,b,c,p,q,r being Point of CLS holds (a=b or a=c or b=c implies [a,b
,c] in the Collinearity of CLS) & (a<>b & [a,b,p] in the Collinearity of CLS &
[a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies
  [p,q,r] in the Collinearity of CLS) by Lm5,Lm6;
  hence thesis by Def3,Def4;
end;

definition
  let IT be non empty CollStr;
  attr IT is proper means
  :Def6:
  ex a,b,c being Point of IT st not a,b,c is_collinear;
end;

registration
  cluster strict proper for CollSp;
  existence
  proof
    reconsider CLS as CollSp by Lm8;
    CLS is proper by Def6,Lm7;
    hence thesis;
  end;
end;

reserve CLSP for proper CollSp;
reserve a,b,c,p,q,r for Point of CLSP;

theorem Th12:
  for p,q holds p<>q implies ex r st not p,q,r is_collinear
proof
  let p,q;
  consider a,b,c such that
A1: not a,b,c is_collinear by Def6;
  assume p<>q;
  then not p,q,a is_collinear or not p,q,b is_collinear or not p,q,c
  is_collinear by A1,Th3;
  hence thesis;
end;

definition
  let CLSP;
  mode LINE of CLSP -> set means
    :Def7:
    ex a,b st a<>b & it=Line(a,b);
  existence
  proof
    consider a,b,c such that
A1: not a,b,c is_collinear by Def6;
    take Line(a,b);
    a<>b by A1,Th2;
    hence thesis;
  end;
end;

reserve P,Q for LINE of CLSP;

theorem
  a=b implies Line(a,b) = the carrier of CLSP
proof
  assume
A1: a=b;
  for x be set holds x in Line(a,b) iff x in the carrier of CLSP
  proof
    let x be set;
    thus x in Line(a,b) implies x in the carrier of CLSP
    proof
      assume x in Line(a,b);
      then ex p st x=p & a,b,p is_collinear;
      then reconsider x as Point of CLSP;
      x is Element of CLSP;
      hence thesis;
    end;
    thus x in the carrier of CLSP implies x in Line(a,b)
    proof
      assume x in the carrier of CLSP;
      then reconsider x as Point of CLSP;
      a,b,x is_collinear by A1,Th2;
      hence thesis;
    end;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  for P ex a,b st a<>b & a in P & b in P
proof
  let P;
  consider a,b such that
A1: a<>b & P = Line(a,b) by Def7;
  take a,b;
  thus thesis by A1,Th10;
end;

theorem
  a <> b implies ex P st a in P & b in P
proof
  assume a<>b;
  then reconsider P = Line(a,b) as LINE of CLSP by Def7;
  take P;
  thus thesis by Th10;
end;

theorem Th16:
  p in P & q in P & r in P implies p,q,r is_collinear
proof
  assume that
A1: p in P & q in P and
A2: r in P;
  consider a,b such that
A3: a<>b and
A4: P = Line(a,b) by Def7;
A5: ex z be Point of CLSP st z=r & a,b,z is_collinear by A2,A4;
  ( ex x be Point of CLSP st x=p & a,b,x is_collinear)& ex y be Point of
  CLSP st y=q & a,b,y is_collinear by A1,A4;
  hence thesis by A3,A5,Th3;
end;

Lm9: for x be set holds x in P implies x is Point of CLSP
proof
  let x be set;
  consider a,b such that
  a<>b and
A1: P = Line(a,b) by Def7;
  assume x in P;
  then ex r be Point of CLSP st r=x & a,b,r is_collinear by A1;
  hence thesis;
end;

theorem Th17:
  P c= Q implies P = Q
proof
  assume
A1: P c= Q;
  Q c= P
  proof
    let r be set;
    consider p,q such that
    p<>q and
A2: P = Line(p,q) by Def7;
    assume
A3: r in Q;
    then reconsider r as Point of CLSP by Lm9;
    p in P & q in P by A2,Th10;
    then p,q,r is_collinear by A1,A3,Th16;
    hence thesis by A2;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th18:
  p<>q & p in P & q in P implies Line(p,q) c= P
proof
  assume that
A1: p<>q and
A2: p in P & q in P;
  let x be set;
  consider a,b such that
  a<>b and
A3: P = Line(a,b) by Def7;
  assume x in Line(p,q);
  then consider r be Point of CLSP such that
A4: r=x and
A5: p,q,r is_collinear;
  a,b,p is_collinear & a,b,q is_collinear by A2,A3,Th11;
  then a,b,r is_collinear by A1,A5,Th9;
  hence thesis by A3,A4;
end;

theorem Th19:
  p<>q & p in P & q in P implies Line(p,q) = P
proof
  assume that
A1: p<>q and
A2: p in P & q in P;
  reconsider Q = Line(p,q) as LINE of CLSP by A1,Def7;
  Q c= P by A1,A2,Th18;
  hence thesis by Th17;
end;

theorem Th20:
  p<>q & p in P & q in P & p in Q & q in Q implies P = Q
proof
  assume that
A1: p<>q and
A2: p in P & q in P and
A3: p in Q & q in Q;
  Line(p,q) = P by A1,A2,Th19;
  hence thesis by A1,A3,Th19;
end;

theorem
  P = Q or P misses Q or ex p st P /\ Q = {p}
proof
A1: (ex a be set st {a} = P /\ Q) implies ex p st P /\ Q = {p}
  proof
    given a be set such that
A2: {a} = P /\ Q;
    a in P /\ Q by A2,TARSKI:def 1;
    then a in P by XBOOLE_0:def 4;
    then reconsider p=a as Point of CLSP by Lm9;
    P /\ Q = {p} by A2;
    hence thesis;
  end;
A3: (ex a,b be set st a<>b & a in P /\ Q & b in P /\ Q) implies P = Q
  proof
    given a,b be set such that
A4: a<>b and
A5: a in P /\ Q & b in P /\ Q;
    a in P & b in P by A5,XBOOLE_0:def 4;
    then reconsider p=a, q=b as Point of CLSP by Lm9;
A6: p in Q & q in Q by A5,XBOOLE_0:def 4;
    p in P & q in P by A5,XBOOLE_0:def 4;
    hence thesis by A4,A6,Th20;
  end;
  P /\ Q = {} or ex a be set st {a} = P /\ Q or ex a,b be set st a<>b & a
  in P /\ Q & b in P /\ Q by Th1;
  hence thesis by A1,A3,XBOOLE_0:def 7;
end;

theorem
  a<>b implies Line(a,b) <> the carrier of CLSP
proof
  assume a<>b;
  then ex r st not a,b,r is_collinear by Th12;
  hence thesis by Th11;
end;