:: Parallelity and Lines in Affine Spaces :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received May 4, 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 DIRAF, SUBSET_1, ANALOAF, INCSP_1, STRUCT_0, TARSKI, AFF_1; notations TARSKI, STRUCT_0, ANALOAF, DIRAF; constructors DIRAF; registrations STRUCT_0; requirements SUBSET, BOOLE; begin reserve AS for AffinSpace; reserve a,a9,b,b9,c,d,o,p,q,r,s,x,y,z,t,u,w for Element of AS; definition let AS,a,b,c; pred LIN a,b,c means :: AFF_1:def 1 a,b // a,c; end; ::$CT theorem :: AFF_1:2 x,y // y,x & x,y // x,y; theorem :: AFF_1:3 x,y // z,z & z,z // x,y; theorem :: AFF_1:4 x,y // z,t implies x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x; theorem :: AFF_1:5 a<>b & ( a,b // x,y & a,b // z,t or a,b // x,y & z,t // a,b or x ,y // a,b & z,t // a,b or x,y // a,b & a,b // z,t ) implies x,y // z,t; theorem :: AFF_1:6 LIN x,y,z implies LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x; theorem :: AFF_1:7 LIN x,x,y & LIN x,y,y & LIN x,y,x; theorem :: AFF_1:8 x<>y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u; theorem :: AFF_1:9 x<>y & LIN x,y,z & x,y // z,t implies LIN x,y,t; theorem :: AFF_1:10 LIN x,y,z & LIN x,y,t implies x,y // z,t; theorem :: AFF_1:11 u<>z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w; theorem :: AFF_1:12 ex x,y,z st not LIN x,y,z; theorem :: AFF_1:13 x<>y implies ex z st not LIN x,y,z; theorem :: AFF_1:14 not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b=b9; :: :: Definition of the Line joining two points :: definition let AS,a,b; func Line(a,b) -> Subset of AS means :: AFF_1:def 2 for x holds x in it iff LIN a,b,x; end; reserve A,C,D,K for Subset of AS; definition let AS,a,b; redefine func Line(a,b); commutativity; end; theorem :: AFF_1:15 a in Line(a,b) & b in Line(a,b); theorem :: AFF_1:16 c in Line(a,b) & d in Line(a,b) & c <>d implies Line(c,d) c= Line(a,b); theorem :: AFF_1:17 c in Line(a,b) & d in Line(a,b) & a<>b implies Line(a,b) c= Line (c,d); :: :: Definition of the Line :: definition let AS,A; attr A is being_line means :: AFF_1:def 3 ex a,b st a <> b & A = Line(a,b); end; registration let AS; cluster being_line for Subset of AS; end; :: Otrzymujemy stad zasadnicze stwierdzenie, ze kazda prosta :: jest jednoznacznie wyznaczona przez swoje dowolne dwa punkty. theorem :: AFF_1:18 A is being_line & C is being_line & a in A & b in A & a in C & b in C implies a=b or A=C; theorem :: AFF_1:19 A is being_line implies ex a,b st a in A & b in A & a<>b; theorem :: AFF_1:20 A is being_line implies ex b st a<>b & b in A; theorem :: AFF_1:21 LIN a,b,c iff ex A st A is being_line & a in A & b in A & c in A; :: :: Definition of the parallelity between segments and lines :: definition let AS,a,b,A; pred a,b // A means :: AFF_1:def 4 ex c,d st c <>d & A=Line(c,d) & a,b // c,d; end; definition let AS,A,C; pred A // C means :: AFF_1:def 5 ex a,b st A=Line(a,b) & a<>b & a,b // C; end; theorem :: AFF_1:22 c in Line(a,b) & a<>b implies (d in Line(a,b) iff a,b // c,d); theorem :: AFF_1:23 A is being_line & a in A implies (b in A iff a,b // A); theorem :: AFF_1:24 a<>b & A=Line(a,b) iff A is being_line & a in A & b in A & a<>b; theorem :: AFF_1:25 A is being_line & a in A & b in A & a<>b & LIN a,b,x implies x in A; theorem :: AFF_1:26 (ex a,b st a,b // A) implies A is being_line; theorem :: AFF_1:27 c in A & d in A & A is being_line & c <>d implies (a,b // A iff a,b // c,d); theorem :: AFF_1:28 a,b // A implies ex c,d st c <>d & c in A & d in A & a,b // c,d; theorem :: AFF_1:29 a<>b implies a,b // Line(a,b); theorem :: AFF_1:30 for A be being_line Subset of AS holds (a,b // A iff ex c,d st c <>d & c in A & d in A & a,b // c,d ); theorem :: AFF_1:31 for A be being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d; theorem :: AFF_1:32 a,b // A & a,b // p,q & a<>b implies p,q // A; theorem :: AFF_1:33 for A be being_line Subset of AS holds a,a // A; theorem :: AFF_1:34 a,b // A implies b,a // A; theorem :: AFF_1:35 a,b // A & not a in A implies not b in A; theorem :: AFF_1:36 A // C implies A is being_line & C is being_line; theorem :: AFF_1:37 A // C iff ex a,b,c,d st a<>b & c <>d & a,b // c,d & A=Line(a,b) & C=Line(c,d); theorem :: AFF_1:38 for A, C be being_line Subset of AS st a in A & b in A & c in C & d in C & a<>b & c<>d holds (A // C iff a,b // c,d); theorem :: AFF_1:39 a in A & b in A & c in C & d in C & A // C implies a,b // c,d; theorem :: AFF_1:40 a in A & b in A & A // C implies a,b // C; theorem :: AFF_1:41 for A being being_line Subset of AS holds A // A; definition let AS; let A,B be being_line Subset of AS; redefine pred A // B; reflexivity; end; theorem :: AFF_1:42 A // C implies C // A; definition let AS,A,C; redefine pred A // C; symmetry; end; theorem :: AFF_1:43 a,b // A & A // C implies a,b // C; theorem :: AFF_1:44 ( A // C & C // D or A // C & D // C or C // A & C // D or C // A & D // C ) implies A // D; theorem :: AFF_1:45 A // C & p in A & p in C implies A=C; theorem :: AFF_1:46 x in K & not a in K & a,b // K implies (a=b or not LIN x,a,b); theorem :: AFF_1:47 a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a=b implies a9=b9; theorem :: AFF_1:48 for A be being_line Subset of AS st a in A & b in A & c in A & a<>b & a,b // c,d holds d in A; theorem :: AFF_1:49 for A be being_line Subset of AS ex C st a in C & A // C; theorem :: AFF_1:50 A // C & A // D & p in C & p in D implies C=D; :: :: Additional theorems :: theorem :: AFF_1:51 A is being_line & a in A & b in A & c in A & d in A implies a,b // c,d; theorem :: AFF_1:52 A is being_line & a in A & b in A implies a,b // A; theorem :: AFF_1:53 a,b // A & a,b // C & a<>b implies A // C; theorem :: AFF_1:54 not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9=b9 implies a9=o & b9=o; theorem :: AFF_1:55 not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9=o implies b9=o; theorem :: AFF_1:56 not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a ,b // a9,x implies b9=x; theorem :: AFF_1:57 for a,b,A holds A is being_line & a in A & b in A & a<>b implies A = Line(a,b); :: :: Facts about Affine Plane :: reserve AP for AffinPlane; reserve a,b,c,d,x,p,q for Element of AP; reserve A,C for Subset of AP; theorem :: AFF_1:58 A is being_line & C is being_line & not A // C implies ex x st x in A & x in C; theorem :: AFF_1:59 A is being_line & not a,b // A implies ex x st x in A & LIN a,b,x; theorem :: AFF_1:60 not a,b // c,d implies ex p st LIN a,b,p & LIN c,d,p;