:: Atlas of Midpoint Algebra
::  by Micha{\l} Muzalewski
::
:: Received June 21, 1991
:: Copyright (c) 1991-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ALGSTR_0, SUBSET_1, MIDSP_1, PRE_TOPC, FUNCT_1,
      ZFMISC_1, STRUCT_0, ROBBINS1, ARYTM_3, QC_LANG1, RLVECT_1, SUPINF_2,
      ARYTM_1, VECTSP_1, RLVECT_2, BINOP_1, MIDSP_2;
 notations XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, BINOP_1, DOMAIN_1, STRUCT_0,
      ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1, MIDSP_1;
 constructors BINOP_1, DOMAIN_1, VECTSP_1, MIDSP_1, RLVECT_1;
 registrations XBOOLE_0, RELSET_1, STRUCT_0, VECTSP_1, MIDSP_1;
 requirements SUBSET, BOOLE;
 definitions VECTSP_1;
 theorems BINOP_1, MIDSP_1, RLVECT_1, VECTSP_1;
 schemes BINOP_1;

begin :: Group of Free Vectors

reserve G for non empty addLoopStr;
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
  x + x;
  coherence;
end;

definition let M,G,w;
  attr w is associating means
  p@q = r iff w.(p,r) = w.(r,q);
end;

theorem Th1:
  w is associating implies p@p = p
proof
A1: w.(p,p) = w.(p,p);
  assume w is associating;
  hence thesis by A1;
end;

reserve S for non empty set;
reserve a,b,b9,c,c9,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

  (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
A1: w is_atlas_of S,G;
  func (a,x).w -> Element of S means
  :Def4:
  w.(a,it) = x;
  existence by A1;
  uniqueness by A1;
end;

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

theorem Th2:
  w is_atlas_of S,G implies w.(a,a) = 0.G
proof
  assume w is_atlas_of S,G;
  then w.(a,a) + w.(a,a) = w.(a,a);
  hence thesis by RLVECT_1:9;
end;

theorem Th3:
  w is_atlas_of S,G & w.(a,b) = 0.G implies a = b
proof
  assume that
A1: w is_atlas_of S,G and
A2: w.(a,b) = 0.G;
  w.(a,b) = w.(a,a) by A1,A2,Th2;
  hence thesis by A1;
end;

theorem Th4:
  w is_atlas_of S,G implies w.(a,b) = -w.(b,a)
proof
  assume
A1: w is_atlas_of S,G;
  then w.(b,a) + w.(a,b) = w.(b,b)
    .= 0.G by A1,Th2;
  then -w.(b,a) = --w.(a,b) by RLVECT_1:6;
  hence thesis by RLVECT_1:17;
end;

theorem Th5:
  w is_atlas_of S,G & w.(a,b) = w.(c,d) implies w.(b,a) = w.(d,c)
proof
  assume that
A1: w is_atlas_of S,G and
A2: w.(a,b) = w.(c,d);
  thus w.(b,a) = -w.(c,d) by A1,A2,Th4
    .= w.(d,c) by A1,Th4;
end;

theorem Th6:
  w is_atlas_of S,G implies for b,x ex a st w.(a,b) = x
proof
  assume
A1: w is_atlas_of S,G;
  let b,x;
  consider a such that
A2: w.(b,a) = -x by A1;
  take a;
  w.(a,b) = -(-x) by A1,A2,Th4
    .= x by RLVECT_1:17;
  hence thesis;
end;

theorem Th7:
  w is_atlas_of S,G & w.(b,a) = w.(c,a) implies b = c
proof
  assume that
A1: w is_atlas_of S,G and
A2: w.(b,a) = w.(c,a);
  w.(a,b) = w.(a,c) by A1,A2,Th5;
  hence thesis by A1;
end;

theorem Th8:
  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 &
  w is associating implies p@q = q@p
proof
  let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
  assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
  set r = p@q;
  w.(p,r) = w.(r,q) by A2;
  then w.(r,p) = w.(q,r) by A1,Th5;
  hence thesis by A2;
end;

theorem Th9:
  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 &
  w is associating implies ex r st r@p = q
proof
  let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
  assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
  consider r such that
A3: w.(r,q) = w.(q,p) by A1,Th6;
  take r;
  thus thesis by A2,A3;
end;

reserve G for add-associative right_zeroed right_complementable Abelian non
  empty addLoopStr;
reserve x for Element of G;

theorem Th10:
  for G being add-associative Abelian non empty addLoopStr, x,y,
  z,t being Element of G holds (x+y)+(z+t) = (x+z)+(y+t)
proof
  let G be add-associative Abelian non empty addLoopStr, x,y,z,t be Element
  of G;
  thus (x+y)+(z+t) = x+(y+(z+t)) by RLVECT_1:def 3
    .= x+(z+(y+t)) by RLVECT_1:def 3
    .= (x+z)+(y+t) by RLVECT_1:def 3;
end;

theorem
  for G being add-associative Abelian non empty addLoopStr, x,y being
  Element of G holds Double (x + y) = Double x + Double y by Th10;

theorem Th12:
  Double (-x) = -Double x
proof
  0.G = Double 0.G by RLVECT_1:def 4
    .= Double (x+-x) by RLVECT_1:def 10
    .= Double x + Double (-x) by Th10;
  hence thesis by RLVECT_1:6;
end;

theorem Th13:
  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 &
w is associating implies for a,b,c,d being Point of M holds (a@b = c@d iff
  w.(a,d) = w.(c,b))
proof
  let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
  assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
  let a,b,c,d be Point of M;
  thus a@b = c@d implies w.(a,d) = w.(c,b)
  proof
    set p = a@b;
    assume a@b = c@d;
    then
A3: w.(c,p) = w.(p,d) by A2;
    w.(a,p) = w.(p,b) by A2;
    hence w.(a,d) = w.(c,p) + w.(p,b) by A1,A3
      .= w.(c,b) by A1;
  end;
  thus w.(a,d) = w.(c,b) implies a@b = c@d
  proof
    set p = a@b;
    assume
A4: w.(a,d) = w.(c,b);
    w.(p,b) + w.(p,d) = w.(a,p) + w.(p,d) by A2
      .= w.(a,d) by A1
      .= w.(p,b) + w.(c,p) by A1,A4;
    then w.(p,d) = w.(c,p) by RLVECT_1:8;
    hence thesis by A2;
  end;
end;

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

theorem Th14:
  w is_atlas_of S,G implies for a,b,b9,c,c9 holds w.(a,b) = w.(b,c
  ) & w.(a,b9) = w.(b9,c9) implies w.(c,c9) = Double w.(b,b9)
proof
  assume
A1: w is_atlas_of S,G;
  let a,b,b9,c,c9;
  assume
A2: w.(a,b) = w.(b,c) & w.(a,b9) = w.(b9,c9);
  thus w.(c,c9) = w.(c,b9) + w.(b9,c9) by A1
    .= w.(c,a) + w.(a,b9) + w.(b9,c9) by A1
    .= w.(c,b) + w.(b,a) + w.(a,b9) + w.(b9,c9) by A1
    .= Double w.(b,a) + w.(a,b9) + w.(a,b9) by A1,A2,Th5
    .= Double w.(b,a) + Double w.(a,b9) by RLVECT_1:def 3
    .= Double (w.(b,a) + w.(a,b9)) by Th10
    .= Double w.(b,b9) by A1;
end;

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

registration
  let M;
  cluster vectgroup(M) -> Abelian add-associative right_zeroed
    right_complementable;
  coherence by MIDSP_1:56;
end;

theorem Th15:
  (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
proof
  set G = vectgroup(M);
  thus for a being set holds a is Element of G iff a is Vector of M
  proof
    let a be set;
    a is Element of G iff a is Element of setvect(M) by MIDSP_1:53;
    hence thesis by MIDSP_1:48;
  end;
  thus 0.G = zerovect(M) by MIDSP_1:55
    .= ID(M) by MIDSP_1:def 16;
  thus for a,b being Element of G, x,y being Vector of M st a=x & b=y holds a+
  b = x+y
  proof
    let a,b be Element of G,x,y be Vector of M such that
A1: a=x & b=y;
    reconsider xx = x, yy = y as Element of setvect(M) by MIDSP_1:48;
    thus a+b = (the addF of G).(a,b) by RLVECT_1:2
      .= (addvect(M)).(xx,yy) by A1,MIDSP_1:54
      .= xx+yy by MIDSP_1:def 14
      .= x+y by MIDSP_1:def 13;
  end;
end;

Lm1: (for a being Element of vectgroup(M) ex x being Element of vectgroup(M)
st Double x = a) & for a being Element of vectgroup(M) holds Double a = 0.
vectgroup(M) implies a = 0.vectgroup(M)
proof
  set G = vectgroup(M);
  set p = the Point of M;
  thus for a being Element of G ex x being Element of G st Double x = a
  proof
    set p = the Point of M;
    let a be Element of G;
    reconsider aa = a as Vector of M by Th15;
    consider q being Point of M such that
A1: aa = vect(p,q) by MIDSP_1:35;
    set xx = vect(p,p@q);
    reconsider x = xx as Element of G by Th15;
    take x;
    xx + xx = aa by A1,MIDSP_1:42;
    hence thesis by Th15;
  end;
  let a be Element of G;
  reconsider aa = a as Vector of M by Th15;
  consider q being Point of M such that
A2: aa = vect(p,q) by MIDSP_1:35;
  consider r being Point of M such that
A3: aa = vect(q,r) by MIDSP_1:35;
  assume Double a = 0.G;
  then aa + aa = 0.G by Th15
    .= ID(M) by Th15;
  then vect(p,q) + vect(q,r) = vect(p,p) by A2,A3,MIDSP_1:38;
  then vect(p,r) = vect(p,p) by MIDSP_1:40;
  then vect(p,q) = vect(q,p) by A2,A3,MIDSP_1:39;
  then
A4: p@p = q@q by MIDSP_1:37;
  p = p@p by MIDSP_1:def 3
    .= q by A4,MIDSP_1:def 3;
  hence a = ID(M) by A2,MIDSP_1:38
    .= 0.G by Th15;
end;

definition
  let IT be non empty addLoopStr;
  attr IT is midpoint_operator means
  :Def5:
  (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;

registration
  cluster midpoint_operator -> Fanoian for non empty addLoopStr;
  coherence
  proof
    let L be non empty addLoopStr;
    assume
A1: L is midpoint_operator;
    let a be Element of L;
    assume a + a = 0.L;
    then Double a = 0.L;
    hence thesis by A1;
  end;
end;

registration
  cluster strict midpoint_operator add-associative right_zeroed
    right_complementable Abelian for non empty addLoopStr;
  existence
  proof
    set M = the MidSp;
    set G = vectgroup(M);
    ( for a being Element of G ex x being Element of G st Double x = a)&
    for a being Element of G holds Double a = 0.G implies a = 0.G by Lm1;
    then G is midpoint_operator;
    hence thesis;
  end;
end;

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

theorem Th16:
  for G being Fanoian add-associative right_zeroed
right_complementable non empty addLoopStr, x being Element of G holds x = -x
  implies x = 0.G
proof
  let G be Fanoian add-associative right_zeroed right_complementable non
  empty addLoopStr, x be Element of G;
A1: -x + x = 0.G by RLVECT_1:5;
  assume x = -x;
  hence thesis by A1,VECTSP_1:def 18;
end;

theorem Th17:
  for G being Fanoian add-associative right_zeroed
  right_complementable Abelian non empty addLoopStr, x,y being Element of G
  holds Double x = Double y implies x = y
proof
  let G be Fanoian add-associative right_zeroed right_complementable Abelian
  non empty addLoopStr, x,y be Element of G;
  assume Double x = Double y;
  then 0.G = (x+x)+-(y+y) by RLVECT_1:def 10
    .= x+x+(-y+-y) by RLVECT_1:31
    .= x+(x+(-y+-y)) by RLVECT_1:def 3
    .= x+(x+-y+-y) by RLVECT_1:def 3
    .= (x+-y)+(x+-y) by RLVECT_1:def 3;
  then -y+x = 0.G by VECTSP_1:def 18;
  hence x = -(-y) by RLVECT_1:6
    .= y by RLVECT_1:17;
end;

definition
  let G be midpoint_operator add-associative right_zeroed right_complementable
  Abelian non empty addLoopStr, x be Element of G;
  func Half x -> Element of G means
  :Def6:
  Double it = x;
  existence by Def5;
  uniqueness by Th17;
end;

theorem
  Half 0.G = 0.G & Half (x+y) = Half x + Half y & (Half x = Half y
  implies x = y) & Half Double x = x
proof
  Double 0.G = 0.G by RLVECT_1:def 4;
  hence Half 0.G = 0.G by Def6;
  Double (Half x + Half y) = Double Half x + Double Half y by Th10
    .= x + Double Half y by Def6
    .= x + y by Def6;
  hence Half (x+y) = Half x + Half y by Def6;
  thus Half x = Half y implies x = y
  proof
    assume Half x = Half y;
    hence x = Double Half y by Def6
      .= y by Def6;
  end;
  thus thesis by Def6;
end;

theorem Th19:
  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
& w is associating implies for a,b,c,d being Point of M holds (a@b)@(c@
  d) = (a@c)@(b@d)
proof
  let M be non empty MidStr, w be Function of [:the carrier of M,the carrier
  of M:],the carrier of G;
  assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
  let a,b,c,d be Point of M;
A3: w.(b,a@b) = w.(b,b@a) by A1,A2,Th8
    .= w.(b@a,a) by A2
    .= w.(a@b,a) by A1,A2,Th8;
  set p = (a@b)@(c@d);
A4: w.(c,c@d) = w.(c@d,d) by A2;
A5: w.(b,b@d) = w.(b@d,d) by A2;
  w.(c,a@c) = w.(c,c@a) by A1,A2,Th8
    .= w.(c@a,a) by A2
    .= w.(a@c,a) by A1,A2,Th8;
  then Double w.(a@c,c@d) = w.(a,d) by A1,A4,Th14
    .= -w.(d,a) by A1,Th4
    .= -Double w.(b@d,a@b) by A1,A5,A3,Th14
    .= Double -w.(b@d,a@b) by Th12
    .= Double w.(a@b,b@d) by A1,Th4;
  then w.(a@c,c@d) = w.(a@b,b@d) by Th17;
  then
A6: w.(a@c,p) + w.(p,c@d) = w.(a@b,b@d) by A1
    .= w.(p,b@d) + w.(a@b,p) by A1;
  w.(a@b,p) = w.(p,c@d) by A2;
  then w.(a@c,p) = w.(p,b@d) by A6,RLVECT_1:8;
  hence thesis by A2;
end;

theorem Th20:
  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
  & w is associating implies M is MidSp
proof
  let M be non empty MidStr, w be Function of [:the carrier of M,the carrier
  of M:],the carrier of G;
  assume w is_atlas_of the carrier of M,G & w is associating;
  then
  for a,b,c,d being Point of M holds a@a = a & a@b = b@a & (a@b)@(c@d) = (
  a@c)@(b@d) & ex x being Point of M st x@a = b by Th1,Th8,Th9,Th19;
  hence thesis by MIDSP_1:def 3;
end;

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

registration
  let M;
  cluster vectgroup(M) -> midpoint_operator;
  coherence
  by Lm1;
end;

definition
  let M,p,q;
  func vector(p,q) -> Element of vectgroup(M) equals
  vect(p,q);
  coherence by Th15;
end;

definition
  let M;
  func vect(M) -> Function of [:the carrier of M,the carrier of M:], the
  carrier of vectgroup(M) means
  :Def8:
  it.(p,q) = vect(p,q);
  existence
  proof
    deffunc F(Point of M,Point of M) = vector($1,$2);
    consider f being Function of [:the carrier of M,the carrier of M:], the
    carrier of vectgroup(M) such that
A1: f.(p,q) = F(p,q) from BINOP_1:sch 4;
    take f;
    f.(p,q) = vect(p,q)
    proof
      thus f.(p,q) = vector(p,q) by A1
        .= vect(p,q);
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f,g be Function of [:the carrier of M,the carrier of M:], the carrier
    of vectgroup(M);
    assume that
A2: f.(p,q) = vect(p,q) and
A3: g.(p,q) = vect(p,q);
    f.(p,q) = g.(p,q)
    proof
      thus f.(p,q) = vect(p,q) by A2
        .= g.(p,q) by A3;
    end;
    hence f = g by BINOP_1:2;
  end;
end;

theorem Th21:
  vect(M) is_atlas_of the carrier of M, vectgroup(M)
proof
  set w = vect(M);
A1: ex q st w.(p,q) = x
  proof
    reconsider xx = x as Vector of M by Th15;
    consider q such that
A2: xx = vect(p,q) by MIDSP_1:35;
    take q;
    thus thesis by A2,Def8;
  end;
A3: w.(p,q) = w.(p,r) implies q = r
  proof
    assume w.(p,q) = w.(p,r);
    then vect(p,q) = w.(p,r) by Def8
      .= vect(p,r) by Def8;
    hence thesis by MIDSP_1:39;
  end;
  w.(p,q) + w.(q,r) = w.(p,r)
  proof
    w.(p,q) = vect(p,q) & w.(q,r) = vect(q,r) by Def8;
    hence w.(p,q) + w.(q,r) = vect(p,q) + vect(q,r) by Th15
      .= vect(p,r) by MIDSP_1:40
      .= w.(p,r) by Def8;
  end;
  hence thesis by A1,A3;
end;

theorem Th22:
  vect(p,q) = vect(r,s) iff p@s = q@r
proof
  thus vect(p,q) = vect(r,s) implies p@s = q@r by MIDSP_1:37;
  thus p@s = q@r implies vect(p,q) = vect(r,s)
  proof
    assume p@s = q@r;
    then p,q @@ r,s by MIDSP_1:def 4;
    then [p,q] ## [r,s] by MIDSP_1:19;
    hence thesis by MIDSP_1:36;
  end;
end;

theorem Th23:
  p@q = r iff vect(p,r) = vect(r,q)
proof
  p@q = r iff p@q = r@r by MIDSP_1:def 3;
  hence thesis by Th22;
end;

::$CT

Lm2: vect(M) is associating
proof
  let p,q,r;
  set w = vect(M);
  w.(p,r) = vect(p,r) & w.(r,q) = vect(r,q) by Def8;
  hence thesis by Th23;
end;

registration let M;
  cluster vect M -> associating;
  coherence by Lm2;
end;

:: Representation Theorem

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

definition
  let S,G,w;
  assume
A1: w is_atlas_of S,G;
  func @(w) -> BinOp of S means
  :Def9:
  w.(a,it.(a,b)) = w.(it.(a,b),b);
  existence
  proof
    defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
    $2);
A2: for a,b ex c st P[a,b,c]
    proof
      let a,b;
      set x = Half w.(a,b);
      consider c such that
A3:   w.(a,c) = x by A1;
      take c;
      x + x = Double x .= w.(a,b) by Def6
        .= x + w.(c,b) by A1,A3;
      hence thesis by A3,RLVECT_1:8;
    end;
    consider o being BinOp of S such that
A4: for a,b holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A2);
    take o;
    thus thesis by A4;
  end;
  uniqueness
  proof
    defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
    $2);
A5: for a,b,c,c9 st P[a,b,c] & P[a,b,c9] holds c = c9
    proof
      let a,b,c,c9 such that
A6:   ( P[a,b,c])& P[a,b,c9];
      w.(c,c9) = w.(c,a) + w.(a,c9) by A1
        .= w.(c9,b) + w.(b,c) by A1,A6,Th5
        .= w.(c9,c) by A1
        .= -w.(c,c9) by A1,Th4;
      then w.(c,c9) = 0.G by Th16;
      hence thesis by A1,Th3;
    end;
    let f,g be BinOp of S such that
A7: ( for a,b holds w.(a,f.(a,b)) = w.(f.(a,b),b))& for a,b holds w.(a
    ,g.(a,b)) = w.(g.(a,b),b);
    for a,b holds f.(a,b) = g.(a,b)
    proof
      let a,b;
      w.(a,f.(a,b)) = w.(f.(a,b),b) & w.(a,g.(a,b)) = w.(g.(a,b),b) by A7;
      hence thesis by A5;
    end;
    hence f = g by BINOP_1:2;
  end;
end;

theorem Th24:
  w is_atlas_of S,G implies for a,b,c holds @(w).(a,b) = c iff w.(
  a,c) = w.(c,b)
proof
  assume
A1: w is_atlas_of S,G;
  let a,b,c;
  thus @(w).(a,b) = c implies w.(a,c) = w.(c,b) by A1,Def9;
  thus w.(a,c) = w.(c,b) implies @(w).(a,b) = c
  proof
    defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
    $2);
    assume
A2: w.(a,c) = w.(c,b);
A3: for a,b,c,c9 st P[a,b,c] & P[a,b,c9] holds c = c9
    proof
      let a,b,c,c9 such that
A4:   ( P[a,b,c])& P[a,b,c9];
      w.(c,c9) = w.(c,a) + w.(a,c9) by A1
        .= w.(c9,b) + w.(b,c) by A1,A4,Th5
        .= w.(c9,c) by A1
        .= -w.(c,c9) by A1,Th4;
      then w.(c,c9) = 0.G by Th16;
      hence thesis by A1,Th3;
    end;
    set c9 = @(w).(a,b);
    P[a,b,c9] by A1,Def9;
    hence thesis by A2,A3;
  end;
end;

registration
  let D be non empty set, M be BinOp of D;
  cluster MidStr(#D,M#) -> non empty;
  coherence;
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
  w;
  coherence;
end;

theorem Th25:
  w is_atlas_of S,G implies Atlas(w) is associating
proof
  assume A1: w is_atlas_of S,G;
  for a,b,c holds a@b = c iff (Atlas(w)).(a,c) = (Atlas(w)).(c,b)
  proof
    let a,b,c;
    @(w).(a,b) = c iff w.(a,c) = w.(c,b) by A1,Th24;
    hence thesis by MIDSP_1:def 1;
  end;
  hence thesis;
end;

definition
  let S,G,w;
  assume
A1: w is_atlas_of S,G;
  func MidSp.w -> strict MidSp equals
  MidStr (# S, @(w) #);
  coherence
  proof
    set M = MidStr(#S,@(w)#), W = Atlas(w);
    W is associating by A1,Th25;
    hence thesis by A1,Th20;
  end;
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 Th26:
  M is MidSp iff ex G st ex w st w is_atlas_of the carrier of M,G
  & w is associating
proof
  hereby
    assume
A1: M is MidSp;
    thus ex G st ex w st w is_atlas_of the carrier of M,G &
    w is associating
    proof
      reconsider M as MidSp by A1;
      set G = vectgroup(M);
      take G;
      ex w being Function of [:the carrier of M,the carrier of M:], the
carrier of G st w is_atlas_of the carrier of M,G & w is associating
      proof
        take vect(M);
        thus thesis by Th21;
      end;
      hence thesis;
    end;
  end;
  given G being midpoint_operator add-associative right_zeroed
right_complementable Abelian non empty addLoopStr, w being Function of [:the
  carrier of M,the carrier of M:],the carrier of G such that
A2: w is_atlas_of the carrier of M,G & w is associating;
  thus thesis by A2,Th20;
end;

definition
  let M be non empty MidStr;
  struct AtlasStr over M
    (# algebra -> non empty addLoopStr,
      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
  :Def12:
  the algebra of IT is midpoint_operator add-associative right_zeroed
  right_complementable Abelian &
  the function of IT is associating &
  the function of IT is_atlas_of the carrier of M,the algebra of IT;
end;

registration
  let M be MidSp;
  cluster ATLAS-like for AtlasStr over M;
  existence
  proof
    consider G being midpoint_operator add-associative right_zeroed
right_complementable Abelian non empty addLoopStr, w being Function of [:the
    carrier of M,the carrier of M:], the carrier of G such that
A1: w is_atlas_of the carrier of M,G & w is associating by Th26;
    take AtlasStr(# G, w #);
    thus thesis by A1;
  end;
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
  (the function of W).(a,b);
  coherence;
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
  (a,x).(the function of W);
  coherence;
end;

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

theorem Th27:
  w is_atlas_of the carrier of M,G & w is associating
  implies (a@c = b1@b2 iff w.(a,c) = w.(a,b1) + w.(a,b2))
proof
  assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
A3: a@c = b1@b2 iff w.(a,b2) = w.(b1,c) by A1,A2,Th13;
  hence a@c = b1@b2 implies w.(a,c) = w.(a,b1) + w.(a,b2) by A1;
  w.(a,c) = w.(a,b1) + w.(b1,c) by A1;
  hence thesis by A3,RLVECT_1:8;
end;

theorem Th28:
  w is_atlas_of the carrier of M,G & w is associating
  implies (a@c = b iff w.(a,c) = Double w.(a,b))
proof
  assume
A1: w is_atlas_of the carrier of M,G & w is associating;
  then reconsider MM = M as MidSp by Th20;
  reconsider bb = b as Point of MM;
  bb@bb = bb by MIDSP_1:def 3;
  hence thesis by A1,Th27;
end;

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
  a@c = b1@b2 iff W.(a,c) = W.(a,b1) + W.(a,b2)
proof
  set w = the function of W, G = the algebra of W;
A1: G is midpoint_operator add-associative right_zeroed right_complementable
  Abelian by Def12;
  w is_atlas_of the carrier of M,G & w is associating by Def12;
  hence thesis by A1,Th27;
end;

theorem
  a@c = b iff W.(a,c) = Double W.(a,b)
proof
  set w = the function of W, G = the algebra of W;
A1: G is midpoint_operator add-associative right_zeroed right_complementable
  Abelian by Def12;
  w is_atlas_of the carrier of M,G & w is associating by Def12;
  hence thesis by A1,Th28;
end;

theorem
  (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)
proof
  set w = the function of W;
  thus for a,x ex b st W.(a,b) = x
  proof
    set w = the function of W;
    let a,x;
    w is_atlas_of the carrier of M,(the algebra of W) by Def12;
    then consider b such that
A1: w.(a,b) = x;
    take b;
    thus thesis by A1;
  end;
  thus for a,b,c holds W.(a,b) = W.(a,c) implies b = c
  proof
    set w = the function of W;
A2: w is_atlas_of (the carrier of M),(the algebra of W) by Def12;
    let a,b,c;
    assume W.(a,b) = W.(a,c);
    hence thesis by A2;
  end;
  let a,b,c;
  w is_atlas_of the carrier of M,(the algebra of W) by Def12;
  hence thesis;
end;

theorem Th32:
  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)
proof
  set w = the function of W, G = the algebra of W;
A1: w is_atlas_of (the carrier of M),G by Def12;
A2: G is midpoint_operator add-associative right_zeroed right_complementable
  Abelian by Def12;
  hence W.(a,a) = 0.W by A1,Th2;
  thus W.(a,b) = 0.W implies a = b by A2,A1,Th3;
  thus W.(a,b) = -W.(b,a) by A2,A1,Th4;
  thus W.(a,b) = W.(c,d) implies W.(b,a) = W.(d,c) by A2,A1,Th5;
  thus for b,x ex a st W.(a,b) = x
  proof
    let b,x;
    consider a such that
A3: w.(a,b) = x by A2,A1,Th6;
    take a;
    thus thesis by A3;
  end;
  thus W.(b,a) = W.(c,a) implies b = c by A2,A1,Th7;
A4: w is associating by Def12;
  hence a@b = c iff W.(a,c) = W.(c,b);
  thus a@b = c@d iff W.(a,d) = W.(c,b) by A2,A4,A1,Th13;
  thus thesis by A1,Def4;
end;

theorem
  (a,0.W).W = a
proof
  W.(a,a) = 0.W by Th32;
  hence thesis by Th32;
end;