:: Atlas of Midpoint Algebra
::  by Micha{\l} Muzalewski
::
:: Received June 21, 1991
:: Copyright (c) 1991-2021 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;


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
:: MIDSP_2:def 1
  x + x;
end;

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

theorem :: MIDSP_2:1
  w is associating implies p@p = p;

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
:: 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
  addLoopStr;
reserve x for Element of G;
reserve w for Function of [:S,S:],the carrier of G;

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

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

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

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

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

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

theorem :: MIDSP_2:8
  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;

theorem :: MIDSP_2:9
  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;

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

theorem :: MIDSP_2:10
  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);

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

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

theorem :: MIDSP_2:13
  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));

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

theorem :: MIDSP_2:14
  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);

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;
end;

theorem :: MIDSP_2:15
  (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 addLoopStr;
  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;

registration
  cluster midpoint_operator -> Fanoian for non empty addLoopStr;
end;

registration
  cluster strict midpoint_operator add-associative right_zeroed
    right_complementable Abelian for non empty addLoopStr;
end;

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

theorem :: MIDSP_2:16
  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;

theorem :: MIDSP_2:17
  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;

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
:: MIDSP_2:def 6

  Double it = x;
end;

theorem :: MIDSP_2:18
  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:19
  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);

theorem :: MIDSP_2:20
  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;

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

registration
  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:21
  vect(M) is_atlas_of the carrier of M, vectgroup(M);

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

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

::$CT


registration let M;
  cluster vect M -> associating;
end;

:: 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:25
  w is_atlas_of S,G implies for a,b,c holds @(w).(a,b) = c iff w.(
  a,c) = w.(c,b);

registration
  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;

theorem :: MIDSP_2:26
  w is_atlas_of S,G implies Atlas(w) is associating;

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:27
  M is MidSp iff ex G st ex w st w is_atlas_of the carrier of M,G
  & w is associating;

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
:: MIDSP_2:def 12

  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;
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;

theorem :: MIDSP_2:28
  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));

theorem :: MIDSP_2:29
  w is_atlas_of the carrier of M,G & w is associating
  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:30
  a@c = b1@b2 iff W.(a,c) = W.(a,b1) + W.(a,b2);

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

theorem :: MIDSP_2:32
  (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:33
  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:34
  (a,0.W).W = a;