The abstract of the Mizar article:

Atlas of Midpoint Algebra

by

Michal Muzalewski

Received June 21, 1991

MML identifier: MIDSP_2

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, MIDSP_1, PRE_TOPC, FUNCT_1, QC_LANG1, ARYTM_1, VECTSP_1,
      RLVECT_2, BINOP_1, MIDSP_2;
 notation XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, BINOP_1, STRUCT_0, PRE_TOPC,
      RLVECT_1, VECTSP_1, MIDSP_1;
 constructors BINOP_1, MIDSP_1, VECTSP_1, MEMBERED, XBOOLE_0;
 clusters MIDSP_1, STRUCT_0, RELSET_1, SUBSET_1, VECTSP_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

                       ::
                       :: GROUP OF FREE VECTORS
                       ::

 reserve G for non empty LoopStr;
 reserve x for Element of G;
 reserve M for non empty MidStr;
 reserve p,q,r for Point of M;
 reserve w for Function of [:the carrier of M,the carrier of M:],
                             the carrier of G;

definition let G,x;
 func Double x -> Element of G equals
:: MIDSP_2:def 1
   x + x;
end;

definition let M,G,w;
 pred M,G are_associated_wrp w means
:: MIDSP_2:def 2
  p@q = r iff w.(p,r) = w.(r,q);
end;

theorem :: MIDSP_2:1
 M,G are_associated_wrp w implies p@p = p;

reserve S for non empty set;
reserve a,b,b',c,c',d for Element of S;
reserve w for Function of [:S,S:],the carrier of G;

definition let S,G,w;
 pred w is_atlas_of S,G means
:: MIDSP_2:def 3
  (for a,x ex b st w.(a,b) = x)
       & (for a,b,c holds w.(a,b) = w.(a,c) implies b = c)
       & for a,b,c holds w.(a,b) + w.(b,c) = w.(a,c);
end;

definition let S,G,w,a,x;
 assume  w is_atlas_of S,G;
 func (a,x).w -> Element of S means
:: MIDSP_2:def 4
  w.(a,it) = x;
end;

reserve G for add-associative right_zeroed right_complementable
    (non empty LoopStr);
reserve x for Element of G;
reserve w for Function of [:S,S:],the carrier of G;

theorem :: MIDSP_2:2
 Double 0.G = 0.G;

canceled;

theorem :: MIDSP_2:4
 w is_atlas_of S,G implies w.(a,a) = 0.G;

theorem :: MIDSP_2:5
 w is_atlas_of S,G & w.(a,b) = 0.G implies a = b;

theorem :: MIDSP_2:6
 w is_atlas_of S,G implies w.(a,b) = -w.(b,a);

theorem :: MIDSP_2:7
 w is_atlas_of S,G & w.(a,b) = w.(c,d) implies w.(b,a) = w.(d,c);

theorem :: MIDSP_2:8
 w is_atlas_of S,G implies for b,x ex a st w.(a,b) = x;

theorem :: MIDSP_2:9
 w is_atlas_of S,G & w.(b,a) = w.(c,a) implies b = c;

theorem :: MIDSP_2:10
 for w being Function of [:the carrier of M,the carrier of M:],
                             the carrier of G holds
      w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
                             implies p@q = q@p;

theorem :: MIDSP_2:11
 for w being Function of [:the carrier of M,the carrier of M:],
                             the carrier of G holds
      w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
                             implies ex r st r@p = q;

reserve G for add-associative right_zeroed right_complementable
   Abelian (non empty LoopStr);
reserve x for Element of G;

canceled;

theorem :: MIDSP_2:13
  for G being add-associative Abelian (non empty LoopStr),
      x,y,z,t being Element of G holds
 (x+y)+(z+t) = (x+z)+(y+t);

theorem :: MIDSP_2:14
  for G being add-associative Abelian (non empty LoopStr),
      x,y being Element of G holds
 Double (x + y) = Double x + Double y;

theorem :: MIDSP_2:15
 Double (-x) = -Double x;

theorem :: MIDSP_2:16
 for w being Function of [:the carrier of M,the carrier of M:],
                             the carrier of G holds
      w is_atlas_of the carrier of M,G & M,G are_associated_wrp w implies
      for a,b,c,d being Point of M holds
                             (a@b = c@d iff w.(a,d) = w.(c,b));

reserve w for Function of [:S,S:],the carrier of G;

theorem :: MIDSP_2:17
 w is_atlas_of S,G implies for a,b,b',c,c' holds
 w.(a,b) = w.(b,c) & w.(a,b') = w.(b',c') implies w.(c,c') = Double w.(b,b');

reserve M for MidSp;
reserve p,q,r,s for Point of M;

definition let M;
 cluster vectgroup(M) -> Abelian add-associative right_zeroed
   right_complementable;
end;

theorem :: MIDSP_2:18
 (for a being set holds a is Element of vectgroup(M)
        iff a is Vector of M)
  & 0.vectgroup(M) = ID(M)
  & for a,b being Element of vectgroup(M),
         x,y being Vector of M st a=x & b=y
      holds a+b = x+y;

definition let IT be non empty LoopStr;
 attr IT is midpoint_operator means
:: MIDSP_2:def 5
  (for a being Element of IT
      ex x being Element of IT st Double x = a)
       & for a being Element of IT
         holds Double a = 0.IT implies a = 0.IT;
end;

definition
  cluster midpoint_operator -> Fanoian (non empty LoopStr);
end;

definition
 cluster strict midpoint_operator add-associative right_zeroed
  right_complementable Abelian (non empty LoopStr);
end;

reserve G for midpoint_operator add-associative right_zeroed
  right_complementable Abelian (non empty LoopStr);
reserve x,y for Element of G;

theorem :: MIDSP_2:19
  for G being Fanoian add-associative right_zeroed
   right_complementable (non empty LoopStr),
      x being Element of G holds
  x = -x implies x = 0.G;

theorem :: MIDSP_2:20
  for G being Fanoian add-associative right_zeroed
   right_complementable Abelian (non empty LoopStr),
      x,y being Element of G holds
  Double x = Double y implies x = y;

definition let G be midpoint_operator add-associative right_zeroed
   right_complementable Abelian (non empty LoopStr),
               x be Element of G;
 func Half x -> Element of G means
:: MIDSP_2:def 6
  Double it = x;
end;

theorem :: MIDSP_2:21
    Half 0.G = 0.G &
  Half (x+y) = Half x + Half y &
  (Half x = Half y implies x = y) &
  Half Double x = x;

theorem :: MIDSP_2:22
 for M being non empty MidStr, w being Function of
      [:the carrier of M,the carrier of M:],the carrier of G holds
      w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
      implies for a,b,c,d being Point of M holds
                     (a@b)@(c@d) = (a@c)@(b@d);

theorem :: MIDSP_2:23
 for M being non empty MidStr, w being Function of
     [:the carrier of M,the carrier of M:],the carrier of G holds
     w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
       implies M is MidSp;

reserve x,y for Element of vectgroup(M);

definition let M;
 cluster vectgroup(M) -> midpoint_operator;
end;

definition let M,p,q;
 func vector(p,q) -> Element of vectgroup(M) equals
:: MIDSP_2:def 7
   vect(p,q);
end;

definition let M;
 func vect(M) -> Function of [:the carrier of M,the carrier of M:],
                             the carrier of vectgroup(M) means
:: MIDSP_2:def 8
  it.(p,q) = vect(p,q);
end;

theorem :: MIDSP_2:24
 vect(M) is_atlas_of the carrier of M, vectgroup(M);

theorem :: MIDSP_2:25
 vect(p,q) = vect(r,s) iff p@s = q@r;

theorem :: MIDSP_2:26
 p@q = r iff vect(p,r) = vect(r,q);

theorem :: MIDSP_2:27
 M,vectgroup(M) are_associated_wrp vect(M);

               ::
               :: REPRESENTATION THEOREM
               ::

reserve w for Function of [:S,S:],the carrier of G;

definition let S,G,w;
 assume  w is_atlas_of S,G;
 func @(w) -> BinOp of S means
:: MIDSP_2:def 9
  w.(a,it.(a,b)) = w.(it.(a,b),b);
end;

theorem :: MIDSP_2:28
 w is_atlas_of S,G implies for a,b,c holds
                                   @(w).(a,b) = c iff w.(a,c) = w.(c,b);

definition let D be non empty set, M be BinOp of D;
 cluster MidStr(#D,M#) -> non empty;
end;

reserve a,b,c for Point of MidStr(#S,@(w)#);

definition let S,G,w;
 func Atlas(w) -> Function of
  [:the carrier of MidStr(#S,@(w)#),the carrier of MidStr(#S,@(w)#):],
  the carrier of G equals
:: MIDSP_2:def 10
  w;
end;

canceled 3;

theorem :: MIDSP_2:32
 w is_atlas_of S,G implies MidStr(#S,@(w)#),G are_associated_wrp Atlas(w);

definition let S,G,w;
 assume  w is_atlas_of S,G;
 func MidSp.w -> strict MidSp equals
:: MIDSP_2:def 11
    MidStr (# S, @(w) #);
end;

reserve M for non empty MidStr;
reserve w for Function of [:the carrier of M,the carrier of M:],
                            the carrier of G;
reserve a,b,b1,b2,c for Point of M;

theorem :: MIDSP_2:33
 M is MidSp iff ex G st ex w
        st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;

definition let M be non empty MidStr;
 struct AtlasStr over M
  (# algebra -> non empty LoopStr,
     function -> Function of [:the carrier of M,the carrier of M:],
                            the carrier of the algebra #);
end;

definition let M be non empty MidStr;
 let IT be AtlasStr over M;
 attr IT is ATLAS-like means
:: MIDSP_2:def 12
     the algebra of IT is midpoint_operator
       add-associative right_zeroed right_complementable Abelian &
     M,the algebra of IT are_associated_wrp the function of IT
     & the function of IT is_atlas_of the carrier of M,the algebra of IT;
end;

definition let M be MidSp;
 cluster ATLAS-like AtlasStr over M;
end;

definition let M be non empty MidSp;
 mode ATLAS of M is ATLAS-like AtlasStr over M;
end;

definition let M be non empty MidStr, W be AtlasStr over M;
 mode Vector of W is Element of the algebra of W;
end;

definition
 let M be MidSp;
 let W be AtlasStr over M;
 let a,b be Point of M;
 func W.(a,b) -> Element of the algebra of W equals
:: MIDSP_2:def 13
   (the function of W).(a,b);
end;

definition
 let M be MidSp;
 let W be AtlasStr over M;
 let a be Point of M;
 let x be Vector of W;
 func (a,x).W -> Point of M equals
:: MIDSP_2:def 14
   (a,x).(the function of W);
end;

definition let M be MidSp, W be ATLAS of M;
 func 0.W -> Vector of W equals
:: MIDSP_2:def 15
   0.(the algebra of W);
end;

:: SOME USEFUL PROPOSITIONS

theorem :: MIDSP_2:34
  w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
        implies (a@c = b1@b2 iff w.(a,c) = w.(a,b1) + w.(a,b2));

theorem :: MIDSP_2:35
 w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
         implies (a@c = b iff w.(a,c) = Double w.(a,b));

 reserve M for MidSp;
 reserve W for ATLAS of M;
 reserve a,b,b1,b2,c,d for Point of M;
 reserve x for Vector of W;

theorem :: MIDSP_2:36
  a@c = b1@b2 iff W.(a,c) = W.(a,b1) + W.(a,b2);

theorem :: MIDSP_2:37
  a@c = b iff W.(a,c) = Double W.(a,b);

 theorem :: MIDSP_2:38
   (for a,x ex b st W.(a,b) = x)
   & (for a,b,c holds W.(a,b) = W.(a,c) implies b = c)
   & for a,b,c holds W.(a,b) + W.(b,c) = W.(a,c);

theorem :: MIDSP_2:39
 W.(a,a) = 0.W
& (W.(a,b) = 0.W implies a = b)
& W.(a,b) = -W.(b,a)
& (W.(a,b) = W.(c,d) implies W.(b,a) = W.(d,c))
& (for b,x ex a st W.(a,b) = x)
& (W.(b,a) = W.(c,a) implies b = c)
& (a@b = c iff W.(a,c) = W.(c,b))
& (a@b = c@d iff W.(a,d) = W.(c,b))
& (W.(a,b) = x iff (a,x).W = b);

theorem :: MIDSP_2:40
  (a,0.W).W = a;