The Mizar abstract of DIRAF

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Ordered Affine Spaces Defined in Terms of Directed Parallelity --- Part I
by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski
Received May 4, 1990
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));
The abstract of the Mizar article:

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