The abstract of the Mizar article:

Parallelity and Lines in Affine Spaces

by

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received May 4, 1990

MML identifier: AFF_1

[ Mizar article, MML identifier index ]

environ

 vocabulary DIRAF, ANALOAF, INCSP_1, AFF_1;
 notation TARSKI, STRUCT_0, ANALOAF, DIRAF;
 constructors DIRAF, XBOOLE_0;
 clusters STRUCT_0, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin
  reserve AS for AffinSpace;
  reserve a,a',b,b',c,d,o,p,q,r,s,x,y,z,t,u,w
                             for Element of AS;

definition let AS; let a,b,c;
 pred LIN a,b,c means
:: AFF_1:def 1
   a,b // a,c;
end;

canceled 9;

theorem :: AFF_1:10
  for a ex b st a<>b;

theorem :: AFF_1:11
 x,y // y,x & x,y // x,y;

theorem :: AFF_1:12
 x,y // z,z & z,z // x,y;

theorem :: AFF_1:13
  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:14
  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:15
  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:16
 LIN x,x,y & LIN x,y,y & LIN x,y,x;

theorem :: AFF_1:17
 x<>y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u;

theorem :: AFF_1:18
 x<>y & LIN x,y,z & x,y // z,t implies LIN x,y,t;

theorem :: AFF_1:19
  LIN x,y,z & LIN x,y,t implies x,y // z,t;

theorem :: AFF_1:20
 u<>z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w;

theorem :: AFF_1:21
  ex x,y,z st not LIN x,y,z;

theorem :: AFF_1:22
    x<>y implies ex z st not LIN x,y,z;

theorem :: AFF_1:23
   not LIN o,a,b & LIN o,b,b' & a,b // a,b' implies b=b';

::
:: 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;

canceled;

theorem :: AFF_1:25
Line(a,b)=Line(b,a);

definition let AS,a,b;
 redefine func Line(a,b);
 commutativity;
end;

theorem :: AFF_1:26
 a in Line(a,b) & b in Line(a,b);

theorem :: AFF_1:27
 c in Line(a,b) & d in Line(a,b) & c <>d implies Line(c,d) c= Line(a,b);

theorem :: AFF_1:28
  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; let A;
 attr A is being_line means
:: AFF_1:def 3
   ex a,b st a<>b & A=Line(a,b);
  synonym A is_line;
end;

:: Otrzymujemy stad zasadnicze stwierdzenie, ze kazda prosta
:: jest jednoznacznie wyznaczona przez swoje dowolne dwa
:: punkty.

canceled;

theorem :: AFF_1:30
  for a,b,A,C holds A is_line & C is_line &
          a in A & b in A & a in C & b in C implies a=b or A=C;

theorem :: AFF_1:31
 A is_line implies ex a,b st a in A & b in A & a<>b;

theorem :: AFF_1:32
 A is_line implies ex b st a<>b & b in A;

theorem :: AFF_1:33
 LIN a,b,c iff ex A st A is_line & a in A & b in A & c in A;

::
::   Definition of the parallelity between segments and lines
::

definition let AS; let a,b; let 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;

canceled 2;

theorem :: AFF_1:36
  (c in Line(a,b) & a<>b) implies (d in Line(a,b) iff a,b // c,d);

theorem :: AFF_1:37
 A is_line & a in A implies (b in A iff a,b // A );

theorem :: AFF_1:38
  (a<>b & A=Line(a,b)) iff
                  (A is_line & a in A & b in A & a<>b);

theorem :: AFF_1:39
 A is_line & a in A & b in A & a<>b & LIN a,b,x implies x in A;

theorem :: AFF_1:40
 (ex a,b st a,b // A) implies A is_line;

theorem :: AFF_1:41
 (c in A & d in A & A is_line & c <>d) implies
                                     (a,b // A iff a,b // c,d);

canceled;

theorem :: AFF_1:43
  a<>b implies a,b // Line(a,b);

theorem :: AFF_1:44
  A is_line implies (a,b // A iff
                (ex c,d st c <>d & c in A & d in A & a,b // c,d));

theorem :: AFF_1:45
   (A is_line & a,b // A & c,d // A) implies a,b // c,d;

theorem :: AFF_1:46
 (a,b // A & a,b // p,q & a<>b) implies p,q // A;

theorem :: AFF_1:47
  A is_line implies a,a // A;

theorem :: AFF_1:48
 a,b // A implies b,a // A;

theorem :: AFF_1:49
   a,b // A & not a in A implies not b in A;

theorem :: AFF_1:50
 A // C implies (A is_line & C is_line);

theorem :: AFF_1:51
 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:52
 (A is_line & C is_line & a in A & b in A & c in C
       & d in C & a<>b & c <>d) implies
                                      (A // C iff a,b // c,d);

theorem :: AFF_1:53
 a in A & b in A & c in C & d in C & A // C implies
                                                  a,b // c,d;

theorem :: AFF_1:54
   a in A & b in A & A // C implies a,b // C;

theorem :: AFF_1:55
 A is_line implies A // A;

theorem :: AFF_1:56
  A // C implies C // A;

definition let AS,A,C;
 redefine pred A // C;
 symmetry;
end;

theorem :: AFF_1:57
 a,b // A & A // C implies a,b // C;

theorem :: AFF_1:58
    ((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:59
  A // C & p in A & p in C implies A=C;

theorem :: AFF_1:60
   x in K & not a in K & a,b // K implies (a=b or not LIN x,a,b);

theorem :: AFF_1:61
   a,b // K & a',b' // K & LIN p,a,a' & LIN p,b,b' & p in K &
                            not a in K & a=b implies a'=b';

theorem :: AFF_1:62
   A is_line & a in A & b in A & c in A & a<>b & a,b // c,d implies d in A;

theorem :: AFF_1:63
   for a, A st A is_line ex C st a in C & A // C;

theorem :: AFF_1:64
    A // C & A // D & p in C & p in D implies C=D;

::
::                     Additional theorems
::

theorem :: AFF_1:65
   A is_line & a in A & b in A & c in A & d in A implies a,b // c,d;

theorem :: AFF_1:66
    A is_line & a in A & b in A implies a,b // A;

theorem :: AFF_1:67
   a,b // A & a,b // C & a<>b implies A // C;

theorem :: AFF_1:68
 not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a'=b'
                                            implies a'=o & b'=o;

theorem :: AFF_1:69
 not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a'=o implies b'=o;

theorem :: AFF_1:70
   not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & LIN o,b,x &
   a,b // a',b' & a,b // a',x implies b'=x;

theorem :: AFF_1:71
   for a,b,A holds A is_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:72
 A is_line & C is_line & not A // C implies
                          ex x st x in A & x in C;

theorem :: AFF_1:73
   A is_line & not a,b // A implies ex x st x in A & LIN a,b,x;

theorem :: AFF_1:74
   not a,b // c,d implies ex p st LIN a,b,p & LIN c,d,p;