Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Parallelity and Lines in Affine Spaces

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

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;

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

::
::

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

::
::

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