:: The Collinearity Structure
:: by Wojciech Skaba
::
:: Received May 9, 1990
:: Copyright (c) 1990-2026 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,
RELAT_2, INCSP_1, NUMBERS, COLLSP, PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, 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 object 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 are_collinear means
[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
let x be object;
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;
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 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 are_collinear
by Def3;
theorem Th3:
a<>b & a,b,p are_collinear & a,b,q are_collinear & a,b,r
are_collinear implies p,q,r are_collinear
by Def4;
theorem Th4:
a,b,c are_collinear implies b,a,c are_collinear & a,c,b are_collinear
proof
assume
A1: a,b,c are_collinear;
then a=b or a<>b & a,b,b are_collinear & a,b,a are_collinear & a,b,c
are_collinear by Th2;
hence b,a,c are_collinear by Th2,Th3;
a=b or a<>b & a,b,a are_collinear & a,b,c are_collinear & a,b,b
are_collinear by A1,Th2;
hence a,c,b are_collinear by Th2,Th3;
end;
theorem
a,b,a are_collinear by Th2;
theorem Th6:
a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear
proof
assume
A1: a<>b & a,b,c are_collinear & a,b,d are_collinear;
a,b,a are_collinear by Th2;
hence thesis by A1,Th3;
end;
theorem
a,b,c are_collinear implies b,a,c are_collinear by Th4;
theorem Th8:
a,b,c are_collinear implies b,c,a are_collinear
proof
assume a,b,c are_collinear;
then b,a,c are_collinear by Th4;
hence thesis by Th4;
end;
theorem Th9:
p<>q & a,b,p are_collinear & a,b,q are_collinear & p,q,r
are_collinear implies a,b,r are_collinear
proof
assume that
A1: p<>q and
A2: a,b,p are_collinear & a,b,q are_collinear and
A3: p,q,r are_collinear;
now
assume
A4: a<>b;
then a,p,q are_collinear by A2,Th6;
then
A5: p,q,a are_collinear by Th8;
a,b,b are_collinear by Th2;
then p,q,b are_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 are_collinear};
correctness;
end;
theorem Th10:
a in Line(a,b) & b in Line(a,b)
proof
a,b,a are_collinear by Th2;
hence a in Line(a,b);
a,b,b are_collinear by Th2;
hence b in Line(a,b);
end;
theorem Th11:
a,b,r are_collinear iff r in Line(a,b)
proof
thus a,b,r are_collinear implies r in Line(a,b);
thus r in Line(a,b) implies a,b,r are_collinear
proof
assume r in Line(a,b);
then ex p st r=p & a,b,p are_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
let x be object;
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;
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 are_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;
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 are_collinear;
end;
registration
cluster strict proper for CollSp;
existence
proof
reconsider CLS as CollSp by Lm8;
CLS is proper by 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 are_collinear
proof
let p,q;
consider a,b,c such that
A1: not a,b,c are_collinear by Def6;
assume p<>q;
then not p,q,a are_collinear or not p,q,b are_collinear or not p,q,c
are_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 are_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 object holds x in Line(a,b) iff x in the carrier of CLSP
proof
let x be object;
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 are_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 are_collinear by A1,Th2;
hence thesis;
end;
end;
hence thesis by TARSKI:2;
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 are_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 are_collinear by A2,A4;
( ex x be Point of CLSP st x=p & a,b,x are_collinear)& ex y be Point of
CLSP st y=q & a,b,y are_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 are_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 object;
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 are_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 object;
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 are_collinear;
a,b,p are_collinear & a,b,q are_collinear by A2,A3,Th11;
then a,b,r are_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 are_collinear by Th12;
hence thesis by Th11;
end;