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

### Ordered Affine Spaces Defined in Terms of Directed Parallelity --- Part I

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

MML identifier: DIRAF
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, ANALOAF, PARSP_1, INCSP_1, REALSET1, DIRAF;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, STRUCT_0,
ANALOAF, REALSET1;
constructors DOMAIN_1, ANALOAF, MEMBERED, XBOOLE_0;
clusters ANALOAF, RELSET_1, STRUCT_0, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x,y for set;
reserve X for non empty set;
reserve a,b,c,d for Element of X;

definition let X;
let R be Relation of [:X,X:];
func lambda(R) -> Relation of [:X,X:] means
:: DIRAF:def 1
for a,b,c,d being Element of X
holds [[a,b],[c,d]] in it iff ([[a,b],[c,d]] in R or [[a,b],[d,c]] in R);
end;

definition let S be non empty AffinStruct;
func Lambda(S) -> strict AffinStruct equals
:: DIRAF:def 2
AffinStruct (# the carrier of S, lambda(the CONGR of S) #);
end;

definition let S be non empty AffinStruct;
cluster Lambda S -> non empty;
end;

reserve S for OAffinSpace;
reserve a,b,c,d,p,q,r,x,y,z,t,u,w for Element of S;

canceled 3;

theorem :: DIRAF:4
x,y // x,y;

theorem :: DIRAF:5
x,y // z,t implies y,x // t,z & z,t // x,y & t,z // y,x;

theorem :: DIRAF:6
z<>t & x,y // z,t & z,t // u,w implies x,y // u,w;

theorem :: DIRAF:7
x,x // y,z & y,z // x,x;

theorem :: DIRAF:8
x,y // z,t & x,y // t,z implies x=y or z=t;

theorem :: DIRAF:9
x,y // x,z iff x,y // y,z or x,z // z,y;

definition let S be non empty AffinStruct;
let a,b,c be Element of S;
pred Mid a,b,c means
:: DIRAF:def 3
a,b // b,c;
end;

canceled;

theorem :: DIRAF:11
x,y // x,z iff Mid x,y,z or Mid x,z,y;

theorem :: DIRAF:12
Mid a,b,a implies a=b;

theorem :: DIRAF:13
Mid a,b,c implies Mid c,b,a;

theorem :: DIRAF:14
Mid x,x,y & Mid x,y,y;

theorem :: DIRAF:15
Mid a,b,c & Mid a,c,d implies Mid b,c,d;

theorem :: DIRAF:16
b<>c & Mid a,b,c & Mid b,c,d implies Mid a,c,d;

theorem :: DIRAF:17
ex z st Mid x,y,z & y<>z;

theorem :: DIRAF:18
Mid x,y,z & Mid y,x,z implies x=y;

theorem :: DIRAF:19
x<>y & Mid x,y,z & Mid x,y,t implies Mid y,z,t or Mid y,t,z;

theorem :: DIRAF:20
x<>y & Mid x,y,z & Mid x,y,t implies Mid x,z,t or Mid x,t,z;

theorem :: DIRAF:21
Mid x,y,t & Mid x,z,t implies Mid x,y,z or Mid x,z,y;

definition let S be non empty AffinStruct;
let a,b,c,d be Element of S;
pred a,b '||' c,d means
:: DIRAF:def 4
a,b // c,d or a,b // d,c;
end;

canceled;

theorem :: DIRAF:23
a,b '||' c,d iff [[a,b],[c,d]] in lambda(the CONGR of S);

theorem :: DIRAF:24
x,y '||' y,x & x,y '||' x,y;

theorem :: DIRAF:25
x,y '||' z,z & z,z '||' x,y;

theorem :: DIRAF:26
x,y '||' x,z implies y,x '||' y,z;

theorem :: DIRAF:27
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 :: DIRAF:28
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 :: DIRAF:29
ex x,y,z st not x,y '||' x,z;

theorem :: DIRAF:30
ex t st x,z '||' y,t & y<>t;

theorem :: DIRAF:31
ex t st x,y '||' z,t & x,z '||' y,t;

theorem :: DIRAF:32
z,x '||' x,t & x<>z implies ex u st y,x '||' x,u & y,z '||' t,u;

definition let S be non empty AffinStruct;
let a,b,c be Element of S;
pred LIN a,b,c means
:: DIRAF:def 5
a,b '||' a,c;
synonym a,b,c is_collinear;
end;

canceled;

theorem :: DIRAF:34
Mid a,b,c implies a,b,c is_collinear;

theorem :: DIRAF:35
a,b,c is_collinear implies Mid a,b,c or Mid b,a,c or Mid a,c,b;

theorem :: DIRAF:36
x,y,z is_collinear implies x,z,y is_collinear & y,x,z is_collinear &
y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear;

theorem :: DIRAF:37
x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear;

theorem :: DIRAF:38
x<>y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear implies
z,t,u is_collinear;

theorem :: DIRAF:39
x<>y & x,y,z is_collinear & x,y '||' z,t implies x,y,t is_collinear;

theorem :: DIRAF:40
x,y,z is_collinear & x,y,t is_collinear implies x,y '||' z,t;

theorem :: DIRAF:41
u<>z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear implies
x,y,w is_collinear;

theorem :: DIRAF:42
ex x,y,z st not x,y,z is_collinear;

theorem :: DIRAF:43
x<>y implies ex z st not x,y,z is_collinear;

reserve AS for non empty AffinStruct;

canceled;

theorem :: DIRAF:45
AS=Lambda(S) implies for a,b,c,d being Element of S,
a',b',c',d' being Element of AS st
a=a' & b=b' & c =c' & d=d' holds
a',b' // c',d' iff a,b '||' c,d;

theorem :: DIRAF:46
AS = Lambda(S) implies
(ex x,y being Element of AS st x<>y) &
(for x,y,z,t,u,w being Element of AS
holds x,y // y,x & x,y // z,z &
(x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) &
(x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of AS st not x,y // x,z) &
(for x,y,z being Element of AS
ex t being Element of AS st x,z // y,t & y<>t) &
(for x,y,z being Element of AS
ex t being Element of AS st x,y // z,t & x,z // y,t) &
(for x,y,z,t being Element of AS st z,x // x,t & x<>z
ex u being Element of AS st y,x // x,u & y,z // t,u);

definition let IT be non empty AffinStruct;
canceled;

attr IT is AffinSpace-like means
:: DIRAF:def 7
(for x,y,z,t,u,w being Element of IT
holds x,y // y,x & x,y // z,z &
(x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) &
(x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of IT st not x,y // x,z) &
(for x,y,z being Element of IT
ex t being Element of IT st x,z // y,t & y<>t) &
(for x,y,z being Element of IT
ex t being Element of IT st x,y // z,t & x,z // y,t) &
(for x,y,z,t being Element of IT st z,x // x,t & x<>z
ex u being Element of IT st y,x // x,u & y,z // t,u);
end;

definition
cluster strict non trivial AffinSpace-like (non empty AffinStruct);
end;

definition
mode AffinSpace is non trivial AffinSpace-like (non empty AffinStruct);
end;

theorem :: DIRAF:47
for AS being AffinSpace holds
(ex x,y being Element of AS st x<>y) &
(for x,y,z,t,u,w being Element of AS holds
(x,y // y,x & x,y // z,z) &
(x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) &
(x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of AS st not x,y // x,z) &
(for x,y,z being Element of AS
ex t being Element of AS st x,z // y,t & y<>t) &
(for x,y,z being Element of AS
ex t being Element of AS st x,y // z,t & x,z // y,t) &
(for x,y,z,t being Element of AS st z,x // x,t & x<>z
ex u being Element of AS st y,x // x,u & y,z // t,u);

theorem :: DIRAF:48
Lambda(S) is AffinSpace;

theorem :: DIRAF:49
((ex x,y being Element of AS st x<>y) &
(for x,y,z,t,u,w being Element of AS
holds x,y // y,x & x,y // z,z &
(x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) &
(x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of AS st not x,y // x,z) &
(for x,y,z being Element of AS
ex t being Element of AS st x,z // y,t & y<>t) &
(for x,y,z being Element of AS
ex t being Element of AS st x,y // z,t & x,z // y,t) &
(for x,y,z,t being Element of AS st z,x // x,t & x<>z
ex u being Element of AS st y,x // x,u & y,z // t,u))
iff AS is AffinSpace;

reserve S for OAffinPlane;
reserve x,y,z,t,u for Element of S;

theorem :: DIRAF:50
not x,y '||' z,t implies ex u st x,y '||' x,u & z,t '||' z,u;

theorem :: DIRAF:51
AS = Lambda(S) implies
for x,y,z,t being Element of AS st
not x,y // z,t ex u being Element of AS
st x,y // x,u & z,t // z,u;

definition let IT be non empty AffinStruct;
attr IT is 2-dimensional means
:: DIRAF:def 8
for x,y,z,t
being Element of IT st not x,y // z,t
ex u being Element of IT st x,y // x,u & z,t // z,u;
end;

definition
cluster strict 2-dimensional AffinSpace;
end;

definition
mode AffinPlane is 2-dimensional AffinSpace;
end;

canceled;

theorem :: DIRAF:53
Lambda(S) is AffinPlane;

theorem :: DIRAF:54
AS is AffinPlane iff
((ex x,y being Element of AS st x<>y) &
(for x,y,z,t,u,w being Element of AS
holds x,y // y,x & x,y // z,z &
(x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) &
(x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of AS st not x,y // x,z) &
(for x,y,z being Element of AS
ex t being Element of AS st x,z // y,t & y<>t) &
(for x,y,z being Element of AS
ex t being Element of AS st x,y // z,t & x,z // y,t) &
(for x,y,z,t being Element of AS st z,x // x,t & x<>z
ex u being Element of AS st y,x // x,u & y,z // t,u) &
(for x,y,z,t being Element of AS st not x,y // z,t
ex u being Element of AS st x,y // x,u & z,t // z,u));
```