:: The Collinearity Structure
:: by Wojciech Skaba
::
:: Received May 9, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let X be set ;
mode Relation3 of X ->  set  means :Def1: :: COLLSP:def 1
it c= [:X,X,X:];
existence
 ex b1 being set st b1 c= [:X,X,X:] ;
end;

:: deftheorem Def1 defines Relation3 COLLSP:def_1_:_
 for X, b2 being set holds
( b2 is Relation3 of X iff b2 c= [:X,X,X:] );

theorem Th1: :: COLLSP:1
for X being set holds
( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b &amp; a in X &amp; b in X ) ) )
proofend;

:: *********************
:: * COLLINEARITY *
:: *********************
definition
attrc1 is strict ;
struct CollStr  ->  1-sorted ;
aggrCollStr(# carrier, Collinearity #) ->  CollStr ;
sel Collinearity c1 ->  Relation3 of the carrier of c1;
end;

registration
cluster non empty strict for CollStr ;
existence
 ex b1 being CollStr st
( not b1 is empty &amp; b1 is strict )
proofend;
end;

definition
let CS be non empty CollStr ;
let a, b, c be Point of CS;
preda,b,c is_collinear  means :Def2: :: COLLSP:def 2
[a,b,c] in the Collinearity of CS;
end;

:: deftheorem Def2 defines is_collinear COLLSP:def_2_:_
 for CS being non empty CollStr
for a, b, c being Point of CS holds
( a,b,c is_collinear iff [a,b,c] in the Collinearity of CS );

set Z = {1};

Lm1:  1 in {1}
by TARSKI:def_1;

Lm2:  {[1,1,1]} c= [:{1},{1},{1}:]
proofend;

reconsider Z = {1} 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__::_thesis:_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_)_&amp;_(_a_<>_b_&amp;_[a,b,p]_in_the_Collinearity_of_CLS_&amp;_[a,b,q]_in_the_Collinearity_of_CLS_&amp;_[a,b,r]_in_the_Collinearity_of_CLS_implies_[p,q,r]_in_the_Collinearity_of_CLS_)_)
let a, b, c, p, q, r be Point of CLS; ::_thesis: ( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) &amp; ( a <> b &amp; [a,b,p] in the Collinearity of CLS &amp; [a,b,q] in the Collinearity of CLS &amp; [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity 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; ::_thesis: [z1,z2,z3] in the Collinearity of CLS
A2: z3 = 1 by TARSKI:def_1;
 ( z1 = 1 &amp; z2 = 1 ) by TARSKI:def_1;
hence  [z1,z2,z3] in the Collinearity of CLS by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) ; ::_thesis: ( a <> b &amp; [a,b,p] in the Collinearity of CLS &amp; [a,b,q] in the Collinearity of CLS &amp; [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS )
thus  ( a <> b &amp; [a,b,p] in the Collinearity of CLS &amp; [a,b,q] in the Collinearity of CLS &amp; [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) by A1; ::_thesis: verum
end;

definition
let IT be non empty CollStr ;
attrIT is reflexive  means :Def3: :: COLLSP:def 3
 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;

:: deftheorem Def3 defines reflexive COLLSP:def_3_:_
 for IT being non empty CollStr holds
( IT is reflexive iff 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 );

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

:: deftheorem Def4 defines transitive COLLSP:def_4_:_
 for IT being non empty CollStr holds
( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b &amp; [a,b,p] in the Collinearity of IT &amp; [a,b,q] in the Collinearity of IT &amp; [a,b,r] in the Collinearity of IT holds
[p,q,r] in the Collinearity of IT );

registration
cluster non empty strict reflexive transitive for CollStr ;
existence
 ex b1 being non empty CollStr st
( b1 is strict &amp; b1 is reflexive &amp; b1 is transitive )
proofend;
end;

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

theorem Th2: :: COLLSP:2
for CLSP being CollSp
for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds
a,b,c is_collinear
proofend;

theorem Th3: :: COLLSP:3
for CLSP being CollSp
for a, b, p, q, r being Point of CLSP st a <> b &amp; a,b,p is_collinear &amp; a,b,q is_collinear &amp; a,b,r is_collinear holds
p,q,r is_collinear
proofend;

theorem Th4: :: COLLSP:4
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
( b,a,c is_collinear &amp; a,c,b is_collinear )
proofend;

theorem :: COLLSP:5
for CLSP being CollSp
for a, b being Point of CLSP holds a,b,a is_collinear by Th2;

theorem Th6: :: COLLSP:6
for CLSP being CollSp
for a, b, c, d being Point of CLSP st a <> b &amp; a,b,c is_collinear &amp; a,b,d is_collinear holds
a,c,d is_collinear
proofend;

theorem :: COLLSP:7
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,a,c is_collinear by Th4;

theorem Th8: :: COLLSP:8
for CLSP being CollSp
for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,c,a is_collinear
proofend;

theorem Th9: :: COLLSP:9
for CLSP being CollSp
for p, q, a, b, r being Point of CLSP st p <> q &amp; a,b,p is_collinear &amp; a,b,q is_collinear &amp; p,q,r is_collinear holds
a,b,r is_collinear
proofend;

:: *******************
:: * LINES *
:: *******************
definition
let CLSP be CollSp;
let a, b be Point of CLSP;
func Line (a,b) ->  set  equals :: COLLSP:def 5
 {  p where p is Point of CLSP : a,b,p is_collinear  }  ;
correctness
coherence
{  p where p is Point of CLSP : a,b,p is_collinear  }  is set ;
;
end;

:: deftheorem  defines Line COLLSP:def_5_:_
 for CLSP being CollSp
for a, b being Point of CLSP holds Line (a,b) =  {  p where p is Point of CLSP : a,b,p is_collinear  }  ;

theorem Th10: :: COLLSP:10
for CLSP being CollSp
for a, b being Point of CLSP holds
( a in Line (a,b) &amp; b in Line (a,b) )
proofend;

theorem Th11: :: COLLSP:11
for CLSP being CollSp
for a, b, r being Point of CLSP holds
( a,b,r is_collinear iff r in Line (a,b) )
proofend;

set Z = {1,2,3};

set RR =  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) &amp; i in {1,2,3} &amp; j in {1,2,3} &amp; k in {1,2,3} )  }  ;

Lm4:   {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) &amp; i in {1,2,3} &amp; j in {1,2,3} &amp; k in {1,2,3} )  }  c= [:{1,2,3},{1,2,3},{1,2,3}:]
proofend;

reconsider Z = {1,2,3} as non empty set by ENUMSET1:def_1;

reconsider RR =  {  [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) &amp; i in {1,2,3} &amp; j in {1,2,3} &amp; k in {1,2,3} )  }  as Relation3 of Z by Def1, Lm4;

reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ;

Lm5:  for a, b, c being Point of CLS holds
( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) &amp; a in Z &amp; b in Z &amp; c in Z ) )
proofend;

Lm6:  for a, b, c, p, q, r being Point of CLS st a <> b &amp; [a,b,p] in the Collinearity of CLS &amp; [a,b,q] in the Collinearity of CLS &amp; [a,b,r] in the Collinearity of CLS holds
[p,q,r] in the Collinearity of CLS
proofend;

Lm7:  not for a, b, c being Point of CLS holds a,b,c is_collinear
proofend;

Lm8:  CLS is CollSp
proofend;

definition
let IT be non empty CollStr ;
attrIT is proper  means :Def6: :: COLLSP:def 6
 not for a, b, c being Point of IT holds a,b,c is_collinear ;
end;

:: deftheorem Def6 defines proper COLLSP:def_6_:_
 for IT being non empty CollStr holds
( IT is proper iff not for a, b, c being Point of IT holds a,b,c is_collinear );

registration
cluster non empty strict reflexive transitive proper for CollStr ;
existence
 ex b1 being CollSp st
( b1 is strict &amp; b1 is proper )
proofend;
end;

theorem Th12: :: COLLSP:12
for CLSP being proper CollSp
for p, q being Point of CLSP st p <> q holds
ex r being Point of CLSP st not p,q,r is_collinear
proofend;

definition
let CLSP be proper CollSp;
mode LINE of CLSP ->  set  means :Def7: :: COLLSP:def 7
 ex a, b being Point of CLSP st
( a <> b &amp; it = Line (a,b) );
existence
 ex b1 being set ex a, b being Point of CLSP st
( a <> b &amp; b1 = Line (a,b) )
proofend;
end;

:: deftheorem Def7 defines LINE COLLSP:def_7_:_
 for CLSP being proper CollSp
for b2 being set holds
( b2 is LINE of CLSP iff ex a, b being Point of CLSP st
( a <> b &amp; b2 = Line (a,b) ) );

theorem :: COLLSP:13
for CLSP being proper CollSp
for a, b being Point of CLSP st a = b holds
Line (a,b) = the carrier of CLSP
proofend;

theorem :: COLLSP:14
for CLSP being proper CollSp
for P being LINE of CLSP ex a, b being Point of CLSP st
( a <> b &amp; a in P &amp; b in P )
proofend;

theorem :: COLLSP:15
for CLSP being proper CollSp
for a, b being Point of CLSP st a <> b holds
ex P being LINE of CLSP st
( a in P &amp; b in P )
proofend;

theorem Th16: :: COLLSP:16
for CLSP being proper CollSp
for p, q, r being Point of CLSP
for P being LINE of CLSP st p in P &amp; q in P &amp; r in P holds
p,q,r is_collinear
proofend;

Lm9:  for CLSP being proper CollSp
for P being LINE of CLSP
for x being set st x in P holds
x is Point of CLSP
proofend;

theorem Th17: :: COLLSP:17
for CLSP being proper CollSp
for P, Q being LINE of CLSP st P c= Q holds
P = Q
proofend;

theorem Th18: :: COLLSP:18
for CLSP being proper CollSp
for p, q being Point of CLSP
for P being LINE of CLSP st p <> q &amp; p in P &amp; q in P holds
Line (p,q) c= P
proofend;

theorem Th19: :: COLLSP:19
for CLSP being proper CollSp
for p, q being Point of CLSP
for P being LINE of CLSP st p <> q &amp; p in P &amp; q in P holds
Line (p,q) = P
proofend;

theorem Th20: :: COLLSP:20
for CLSP being proper CollSp
for p, q being Point of CLSP
for P, Q being LINE of CLSP st p <> q &amp; p in P &amp; q in P &amp; p in Q &amp; q in Q holds
P = Q
proofend;

theorem :: COLLSP:21
for CLSP being proper CollSp
for P, Q being LINE of CLSP holds
( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
proofend;

theorem :: COLLSP:22
for CLSP being proper CollSp
for a, b being Point of CLSP st a <> b holds
Line (a,b) <> the carrier of CLSP
proofend;