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

### Semi-Affine Space

by
Eugeniusz Kusak, and

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

```environ

vocabulary ANALOAF, DIRAF, INCSP_1, PARSP_2, FDIFF_1, SEMI_AF1;
notation STRUCT_0, ANALOAF, DIRAF;
constructors AFF_1, XBOOLE_0;
clusters ANALOAF, ZFMISC_1, XBOOLE_0;

begin

definition let IT be non empty AffinStruct;
attr IT is Semi_Affine_Space-like means
:: SEMI_AF1:def 1
(for a,b being Element of IT holds a,b // b,a) &
(for a,b,c being Element of IT holds a,b // c,c) &
(for a,b,p,q,r,s being Element of IT holds
( a<>b & a,b // p,q & a,b // r,s implies p,q // r,s )) &
(for a,b,c being Element of IT holds
( a,b // a,c implies b,a // b,c )) &
(ex a,b,c being Element of IT st not a,b // a,c) &
(for a,b,p being Element of IT
ex q being Element of IT st
( a,b // p,q & a,p // b,q )) &
(for o,a being Element of IT holds
(ex p being Element of IT st
(for b,c being Element of IT holds o,a // o,p &
(ex d being Element of IT st
( o,p // o,b implies o,c // o,d & p,c // b,d ))))) &
(for o,a,a',b,b',c,c' being Element of IT holds
( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' &
o,c // o,c' & a,b // a',b' & a,c // a',c' implies
b,c // b',c' )) &
(for a,a',b,b',c,c' being Element of IT holds
( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' &
a,b // a',b' & a,c // a',c' implies b,c // b',c' )) &
(for a1,a2,a3,b1,b2,b3 being Element of IT holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 )) &
(for a,b,c,d being Element of IT holds
( not a,b // a,c & a,b // c,d & a,c // b,d implies
not a,d // b,c ));
end;

definition
cluster Semi_Affine_Space-like (non empty AffinStruct);
end;

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

::
::                        AXIOMS OF SEMI_AFFINE SPACE
::

reserve SAS for Semi_Affine_Space;
reserve a,a',a1,a2,a3,a4,b,b',c,c',d,d',d1,d2,o,p,p1,p2,q,r,r1,r2,s,x,
y,t,z for Element of SAS;

canceled 11;

theorem :: SEMI_AF1:12
a,b // a,b;

theorem :: SEMI_AF1:13
a,b // c,d implies c,d // a,b;

theorem :: SEMI_AF1:14
a,a // b,c;

theorem :: SEMI_AF1:15
a,b // c,d implies b,a // c,d;

theorem :: SEMI_AF1:16
a,b // c,d implies a,b // d,c;

theorem :: SEMI_AF1:17
a,b // c,d implies
b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b &
d,c // a,b & c,d // b,a & d,c // b,a;

theorem :: SEMI_AF1:18
a,b // a,c implies
a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a &
c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b &
b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b &
c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a &
b,c // c,a & c,b // a,c & b,c // a,c;

canceled;

theorem :: SEMI_AF1:20
a<>b & p,q // a,b & a,b // r,s implies p,q // r,s;

theorem :: SEMI_AF1:21
not a,b // a,d implies a<>b & b<>d & d<>a;

theorem :: SEMI_AF1:22
not a,b // p,q implies a<>b & p<>q;

theorem :: SEMI_AF1:23
a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c;

canceled;

theorem :: SEMI_AF1:25
not a,b // a,c & p<>q implies not p,q // p,a or not p,q // p,b or
not p,q // p,c;

theorem :: SEMI_AF1:26
p<>q implies ex r st not p,q // p,r;

canceled;

theorem :: SEMI_AF1:28
not a,b // a,c implies not a,b // c,a & not b,a // a,c & not b,a // c,a &
not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a &
not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b &
not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a &
not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c &
not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b;

theorem :: SEMI_AF1:29
not a,b // c,d & a,b // p,q & c,d // r,s & p<>q & r<>s implies
not p,q // r,s;

theorem :: SEMI_AF1:30
not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p<>q implies
not p,q // p,r;

theorem :: SEMI_AF1:31
not a,b // a,c & a,c // p,r & b,c // p,r implies p=r;

theorem :: SEMI_AF1:32
not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1=r2;

theorem :: SEMI_AF1:33
not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 &
b,c // q,r2 implies r1=r2;

theorem :: SEMI_AF1:34
a=b or c =d or (a=c & b=d) or (a=d & b=c) implies a,b // c,d;

theorem :: SEMI_AF1:35
a=b or a=c or b=c implies a,b // a,c;

::
::          BASIC FACTS ABOUT  COLLINEARITY RELATION
::

definition let SAS,a,b,c;
pred a,b,c is_collinear means
:: SEMI_AF1:def 2
a,b // a,c;
end;

canceled;

theorem :: SEMI_AF1:37
a1,a2,a3 is_collinear implies a1,a3,a2 is_collinear & a2,a1,a3
is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1
is_collinear;

canceled;

theorem :: SEMI_AF1:39
not a,b,c is_collinear & a,b // p,q & a,c // p,r & p<>q & p<>r
implies not
p,q,r is_collinear;

theorem :: SEMI_AF1:40
a=b or b=c or c =a implies a,b,c is_collinear;

theorem :: SEMI_AF1:41
p<>q implies ex r st not p,q,r is_collinear;

theorem :: SEMI_AF1:42
a,b,c is_collinear & a,b,d is_collinear implies a,b // c,d;

theorem :: SEMI_AF1:43
not a,b,c is_collinear & a,b // c,d implies not a,b,d is_collinear;

theorem :: SEMI_AF1:44
not a,b,c is_collinear & a,b // c,d & c <>d & c,d,x is_collinear
implies not a,b,x is_collinear
;

theorem :: SEMI_AF1:45
not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear implies
o=x;

theorem :: SEMI_AF1:46
o<>a & o<>b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b'
is_collinear implies a,b // a',b';

canceled;

theorem :: SEMI_AF1:48
not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1
is_collinear & c,d,p2 is_collinear implies p1=p2;

theorem :: SEMI_AF1:49
a<>b & a,b,c is_collinear & a,b // c,d implies a,c // b,d;

theorem :: SEMI_AF1:50
a<>b & a,b,c is_collinear & a,b // c,d implies c,b // c,d;

theorem :: SEMI_AF1:51
not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear &
o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d1 & a,c // b,d2 implies d1=d2;

theorem :: SEMI_AF1:52
a<>b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear;

::
::                              PARALLELOGRAM
::

definition let SAS,a,b,c,d;
pred parallelogram a,b,c,d means
:: SEMI_AF1:def 3
not a,b,c is_collinear & a,b // c,d & a,c // b,d;
end;

canceled;

theorem :: SEMI_AF1:54
parallelogram a,b,c,d implies a<>b & a<>c & c <>b & a<>d & b<>d & c <>d;

theorem :: SEMI_AF1:55
parallelogram a,b,c,d implies not a,b,c is_collinear & not b,a,d
is_collinear & not c,d,a is_collinear & not d,c,b is_collinear;

theorem :: SEMI_AF1:56
parallelogram a1,a2,a3,a4 implies not a1,a2,a3 is_collinear &
not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear &
not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear &
not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear &
not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear &
not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear &
not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear &
not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear &
not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear &
not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear &
not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear &
not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear &
not a4,a3,a2 is_collinear;

theorem :: SEMI_AF1:57
parallelogram a,b,c,d implies not a,b,x is_collinear or not c,d,x
is_collinear;

theorem :: SEMI_AF1:58
parallelogram a,b,c,d implies parallelogram a,c,b,d;

theorem :: SEMI_AF1:59
parallelogram a,b,c,d implies parallelogram c,d,a,b;

theorem :: SEMI_AF1:60
parallelogram a,b,c,d implies parallelogram b,a,d,c;

theorem :: SEMI_AF1:61
parallelogram a,b,c,d implies parallelogram a,c,b,d & parallelogram
c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram
d,b,c,a & parallelogram b,d,a,c;

theorem :: SEMI_AF1:62
not a,b,c is_collinear implies ex d st parallelogram a,b,c,d;

theorem :: SEMI_AF1:63
parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1=d2;

theorem :: SEMI_AF1:64
parallelogram a,b,c,d implies not a,d // b,c;

theorem :: SEMI_AF1:65
parallelogram a,b,c,d implies not parallelogram a,b,d,c;

theorem :: SEMI_AF1:66
a<>b implies ex c st a,b,c is_collinear & c <>a & c <>b;

theorem :: SEMI_AF1:67
parallelogram a,a',b,b' & parallelogram a,a',c,c' implies b,c // b',c';

theorem :: SEMI_AF1:68
not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram
a,a',c,c' implies parallelogram b,b',c,c';

theorem :: SEMI_AF1:69
a,b,c is_collinear & b<>c & parallelogram a,a',b,b' & parallelogram
a,a',c,c' implies parallelogram b,b',c,c';

theorem :: SEMI_AF1:70
parallelogram a,a',b,b' & parallelogram a,a',c,c' & parallelogram
b,b',d,d' implies c,d // c',d';

theorem :: SEMI_AF1:71
a<>d implies ex b,c st parallelogram a,b,c,d;

::
::                                 CONGRUENCE
::

definition let SAS,a,b,r,s;
pred congr a,b,r,s means
:: SEMI_AF1:def 4
(a=b & r =s) or (ex p,q st parallelogram p,q,a,b &
parallelogram p,q,r,s);
end;

canceled;

theorem :: SEMI_AF1:73
congr a,a,b,c implies b=c;

theorem :: SEMI_AF1:74
congr a,b,c,c implies a=b;

theorem :: SEMI_AF1:75
congr a,b,b,a implies a=b;

theorem :: SEMI_AF1:76
congr a,b,c,d implies a,b // c,d;

theorem :: SEMI_AF1:77
congr a,b,c,d implies a,c // b,d;

theorem :: SEMI_AF1:78
congr a,b,c,d & not a,b,c is_collinear implies parallelogram a,b,c,d;

theorem :: SEMI_AF1:79
parallelogram a,b,c,d implies congr a,b,c,d;

theorem :: SEMI_AF1:80
congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b implies
parallelogram r,s,c,d;

theorem :: SEMI_AF1:81
congr a,b,c,x & congr a,b,c,y implies x=y;

theorem :: SEMI_AF1:82
ex d st congr a,b,c,d;

canceled;

theorem :: SEMI_AF1:84
congr a,b,a,b;

theorem :: SEMI_AF1:85
congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d;

theorem :: SEMI_AF1:86
congr a,b,c,d implies congr c,d,a,b;

theorem :: SEMI_AF1:87
congr a,b,c,d implies congr b,a,d,c;

theorem :: SEMI_AF1:88
congr a,b,c,d implies congr a,c,b,d;

theorem :: SEMI_AF1:89
congr a,b,c,d implies congr c,d,a,b & congr b,a,d,c & congr a,c,b,d &
congr d,c,b,a & congr b,d,a,c & congr c,a,d,b &
congr d,b,c,a;

theorem :: SEMI_AF1:90
congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s;

theorem :: SEMI_AF1:91
congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q;

theorem :: SEMI_AF1:92
congr a,o,o,p & congr b,o,o,q implies congr a,b,q,p;

theorem :: SEMI_AF1:93
congr b,a,p,q & congr c,a,p,r implies b,c // q,r;

theorem :: SEMI_AF1:94
congr a,o,o,p & congr b,o,o,q implies a,b // p,q;

::
::                          A VECTOR' GROUP
::

definition let SAS,a,b,o;
func sum(a,b,o) -> Element of SAS means
:: SEMI_AF1:def 5
congr o,a,b,it;
end;

definition let SAS,a,o;
func opposite(a,o) -> Element of SAS means
:: SEMI_AF1:def 6
sum(a,it,o) = o;
end;

definition let SAS,a,b,o;
func diff(a,b,o) -> Element of SAS equals
:: SEMI_AF1:def 7
sum(a,opposite(b,o),o);
end;

canceled 4;

theorem :: SEMI_AF1:99
sum(a,o,o)=a;

theorem :: SEMI_AF1:100
ex x st sum(a,x,o)=o;

theorem :: SEMI_AF1:101
sum(sum(a,b,o),c,o)=sum(a,sum(b,c,o),o);
theorem :: SEMI_AF1:102
sum(a,b,o)=sum(b,a,o);

theorem :: SEMI_AF1:103
sum(a,a,o)=o implies a=o;

theorem :: SEMI_AF1:104
sum(a,x,o)=sum(a,y,o) implies x=y;

canceled;

theorem :: SEMI_AF1:106
congr a,o,o,opposite(a,o);

theorem :: SEMI_AF1:107
opposite(a,o)=opposite(b,o) implies a=b;

theorem :: SEMI_AF1:108
a,b // opposite(a,o),opposite(b,o);

theorem :: SEMI_AF1:109
opposite(o,o)=o;

theorem :: SEMI_AF1:110
p,q // sum(p,r,o),sum(q,r,o);

theorem :: SEMI_AF1:111
p,q // r,s implies p,q // sum(p,r,o),sum(q,s,o);

canceled;

theorem :: SEMI_AF1:113
diff(a,b,o)=o iff a=b;

theorem :: SEMI_AF1:114
o,diff(b,a,o) // a,b;

theorem :: SEMI_AF1:115
o,diff(b,a,o),diff(d,c,o) is_collinear iff a,b // c,d;

::
::                       A TRAPEZIUM RELATION
::

definition let SAS,a,b,c,d,o;
pred trap a,b,c,d,o means
:: SEMI_AF1:def 8
not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear &
a,c // b,d;
end;

definition let SAS,o,p;
pred qtrap o,p means
:: SEMI_AF1:def 9
for b,c holds (ex d st ( o,p,b is_collinear implies
o,c,d is_collinear & p,c // b,d));
end;

canceled 2;

theorem :: SEMI_AF1:118
trap a,b,c,d,o implies o<>a & a<>c & c <>o;

theorem :: SEMI_AF1:119
trap a,b,c,x,o & trap a,b,c,y,o implies x=y;

theorem :: SEMI_AF1:120
not o,a,b is_collinear implies trap a,o,b,o,o;

theorem :: SEMI_AF1:121
trap a,b,c,d,o implies trap c,d,a,b,o;

theorem :: SEMI_AF1:122
o<>b & trap a,b,c,d,o implies o<>d;

theorem :: SEMI_AF1:123
o<>b & trap a,b,c,d,o implies not o,b,d is_collinear;

theorem :: SEMI_AF1:124
o<>b & trap a,b,c,d,o implies trap b,a,d,c,o;

theorem :: SEMI_AF1:125
(o=b or o=d) & trap a,b,c,d,o implies o=b & o=d;

theorem :: SEMI_AF1:126
trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r;

theorem :: SEMI_AF1:127
trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear implies
trap b,q,c,r,o;

theorem :: SEMI_AF1:128
trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s;

theorem :: SEMI_AF1:129
for o,a holds (ex p st o,a,p is_collinear & qtrap o,p);

theorem :: SEMI_AF1:130
ex x,y,z st x<>y & y<>z & z<>x;

theorem :: SEMI_AF1:131
qtrap o,p implies o<>p;

theorem :: SEMI_AF1:132
qtrap o,p implies ex q st not o,p,q is_collinear & qtrap o,q;

theorem :: SEMI_AF1:133
not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p implies
ex d st trap p,b,c,d,o;
```