:: The Collinearity Structure :: by Wojciech Skaba :: :: Received May 9, 1990 :: Copyright (c) 1990-2017 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;