The Mizar abstract of SEMI

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Semi-Affine Space
by
Eugeniusz Kusak, and
Krzysztof Radziszewski
Received November 30, 1990
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;
The abstract of the Mizar article:

Semi-Affine Space
