:: Midpoint algebras
::  by Micha{\l} Muzalewski
::
:: Received November 26, 1989
:: Copyright (c) 1990-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 STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, QC_LANG1, FUNCT_1,
      FUNCT_5, ZFMISC_1, MCART_1, RELAT_1, VECTSP_1, ARYTM_3, ARYTM_1,
      ALGSTR_0, SUPINF_2, RLVECT_1, MIDSP_1, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, MCART_1, DOMAIN_1,
      ORDINAL1, FUNCT_2, FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1;
 constructors BINOP_1, DOMAIN_1, RLVECT_1, FUNCT_5, RELSET_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin :: PRELIMINARY

definition
  struct(1-sorted) MidStr (# carrier -> set, MIDPOINT -> BinOp of the carrier
  #);
end;

registration
  cluster non empty for MidStr;
end;

reserve MS for non empty MidStr;
reserve a, b for Element of MS;

definition
  let MS,a,b;
  func a@b -> Element of MS equals
:: MIDSP_1:def 1
  (the MIDPOINT of MS).(a,b);
end;

definition
  func Example -> MidStr equals
:: MIDSP_1:def 2
  MidStr (# {0}, op2 #);
end;

registration
  cluster Example -> strict non empty;
end;

theorem :: MIDSP_1:1
  the carrier of Example = {{}};

theorem :: MIDSP_1:2
  the MIDPOINT of Example = op2;

theorem :: MIDSP_1:3
  for a,b being Element of Example holds a@b = op2.(a,b);

theorem :: MIDSP_1:4
  for a,b,c,d being Element of Example holds a@a = a & a@b = b@a &
  (a@b)@(c@d) = (a@c)@(b@d) & ex x being Element of Example st x@a = b;

:: A. MIDPOINT ALGEBRAS

definition
  let IT be non empty MidStr;
  attr IT is MidSp-like means
:: MIDSP_1:def 3

  for a,b,c,d being Element of IT holds a@a
= a & a@b = b@a & (a@b)@(c@d) = (a@c)@(b@d) & ex x being Element of IT st x@a =
  b;
end;

registration
  cluster strict MidSp-like for non empty MidStr;
end;

definition
  mode MidSp is MidSp-like non empty MidStr;
end;

definition
  let M be MidSp, a, b be Element of M;
  redefine func a@b;
  commutativity;
end;

reserve M for MidSp;
reserve a,b,c,d,a9,b9,c9,d9,x,y,x9 for Element of M;

theorem :: MIDSP_1:5
  (a@b)@c = (a@c)@(b@c);

theorem :: MIDSP_1:6  :: right-self-distributivity
  a@(b@c) = (a@b)@(a@c);

theorem :: MIDSP_1:7  :: left-self-distributivity
  a@b = a implies a = b;

theorem :: MIDSP_1:8
  x@a = x9@a implies x = x9;

theorem :: MIDSP_1:9 :: right-cancellation-law
  a@x = a@x9 implies x = x9;

:: left-cancellation-law
:: B. CONGRUENCE RELATION

definition
  let M,a,b,c,d;
  pred a,b @@ c,d means
:: MIDSP_1:def 4 :: bound-vectors ab, cd are equivalent

  a@d = b@c;
end;

theorem :: MIDSP_1:10
  a,a @@ b,b;

theorem :: MIDSP_1:11
  a,b @@ c,d implies c,d @@ a,b;

theorem :: MIDSP_1:12
  a,a @@ b,c implies b = c;

theorem :: MIDSP_1:13
  a,b @@ c,c implies a = b;

theorem :: MIDSP_1:14
  a,b @@ a,b;

theorem :: MIDSP_1:15
  ex d st a,b @@ c,d;

theorem :: MIDSP_1:16
  a,b @@ c,d & a,b @@ c,d9 implies d = d9;

theorem :: MIDSP_1:17
  x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d;

theorem :: MIDSP_1:18
  a,b @@ a9,b9 & b,c @@ b9,c9 implies a,c @@ a9,c9;

:: C. BOUND-VECTORS

reserve p,q,r,p9,q9 for Element of [:the carrier of M,the carrier of M:];

definition
  let M,p,q;
  pred p ## q means
:: MIDSP_1:def 5

  p`1,p`2 @@ q`1,q`2;
  reflexivity;
  symmetry;
end;

theorem :: MIDSP_1:19
  a,b @@ c,d implies [a,b] ## [c,d];

theorem :: MIDSP_1:20
  [a,b] ## [c,d] implies a,b @@ c,d;

theorem :: MIDSP_1:21
  p ## q & p ## r implies q ## r;

theorem :: MIDSP_1:22
  p ## r & q ## r implies p ## q;

theorem :: MIDSP_1:23
  p ## q & q ## r implies p ## r;

theorem :: MIDSP_1:24
  p ## q implies (r ## p iff r ## q);

theorem :: MIDSP_1:25
  for p holds { q : q ## p } is non empty Subset of [:the carrier
  of M,the carrier of M:];

:: D.  ( FREE ) VECTORS

definition
  let M,p;
  func p~ -> Subset of [:the carrier of M,the carrier of M:] equals
:: MIDSP_1:def 6
  { q : q ## p};
end;

registration
  let M,p;
  cluster p~ -> non empty;
end;

theorem :: MIDSP_1:26
  for p holds r in p~ iff r ## p;

theorem :: MIDSP_1:27
  p ## q implies p~ = q~;

theorem :: MIDSP_1:28
  p~ = q~ implies p ## q;

theorem :: MIDSP_1:29
  [a,b]~ = [c,d]~ implies a@d = b@c;

theorem :: MIDSP_1:30
  p in p~;

definition
  let M;
  mode Vector of M -> non empty Subset of [:the carrier of M,the carrier of M
    :] means
:: MIDSP_1:def 7

    ex p st it = p~;
end;

reserve u,v,w,u9,w9 for Vector of M;

definition
  let M,p;
  redefine func p~ -> Vector of M;
end;

theorem :: MIDSP_1:31
  ex u st for p holds p in u iff p`1 = p`2;

definition
  let M;
  func ID(M) -> Vector of M equals
:: MIDSP_1:def 8 :: zero vector
  { p : p`1 = p`2 };
end;

theorem :: MIDSP_1:32
  ID(M) = [b,b]~;

theorem :: MIDSP_1:33
  (ex p,q st u = p~ & v = q~ & p`2 = q`1 & w = [p`1,q`2]~)& (ex p,
  q st u = p~ & v = q~ & p`2 = q`1 & w9 = [p`1,q`2]~) implies w = w9;

definition
  let M,u,v;
  func u + v -> Vector of M means
:: MIDSP_1:def 9

  ex p,q st u = p~ & v = q~ & p`2 = q `1 & it = [p`1,q`2]~;
end;

:: E. ATLAS

theorem :: MIDSP_1:34
  ex b st u = [a,b]~;

definition
  let M,a,b;
  func vect(a,b) -> Vector of M equals
:: MIDSP_1:def 10
  [a,b]~;
end;

theorem :: MIDSP_1:35
  ex b st u = vect(a,b);

theorem :: MIDSP_1:36
  [a,b] ## [c,d] implies vect(a,b) = vect(c,d);

theorem :: MIDSP_1:37
  vect(a,b) = vect(c,d) implies a@d = b@c;

theorem :: MIDSP_1:38
  ID(M) = vect(b,b);

theorem :: MIDSP_1:39
  vect(a,b) = vect(a,c) implies b = c;

theorem :: MIDSP_1:40
  vect(a,b) + vect(b,c) = vect(a,c);

:: F. VECTOR GROUPS

theorem :: MIDSP_1:41
  [a,a@b] ## [a@b,b];

theorem :: MIDSP_1:42
  vect(a,a@b) + vect(a,a@b) = vect(a,b);

theorem :: MIDSP_1:43
  (u+v)+w = u+(v+w);

theorem :: MIDSP_1:44
  u+ID(M) = u;

theorem :: MIDSP_1:45
  ex v st u+v = ID(M);

theorem :: MIDSP_1:46
  u+v = v+u;

theorem :: MIDSP_1:47
  u + v = u + w implies v = w;

definition
  let M,u;
  func -u -> Vector of M means
:: MIDSP_1:def 11
  u + it = ID(M);
end;

reserve X for Subset of [:the carrier of M,the carrier of M:];

definition
  let M;
  func setvect(M) -> set equals
:: MIDSP_1:def 12
  { X : X is Vector of M};
end;

reserve x for set;

theorem :: MIDSP_1:48
  x is Vector of M iff x in setvect(M);

registration
  let M;
  cluster setvect(M) -> non empty;
end;

reserve u1,v1,w1,W,W1,W2,T for Element of setvect(M);

definition
  let M,u1,v1;
  func u1 + v1 -> Element of setvect(M) means
:: MIDSP_1:def 13

  for u,v holds u1 = u & v1 = v implies it = u + v;
end;

theorem :: MIDSP_1:49
  u1 + v1 = v1 + u1;

theorem :: MIDSP_1:50
  (u1 + v1) + w1 = u1 + (v1 + w1);

definition
  let M;
  func addvect(M) -> BinOp of setvect(M) means
:: MIDSP_1:def 14

  for u1,v1 holds it.(u1, v1) = u1 + v1;
end;

theorem :: MIDSP_1:51
  for W ex T st W + T = ID(M);

theorem :: MIDSP_1:52
  for W,W1,W2 st W + W1 = ID(M) & W + W2 = ID(M) holds W1 = W2;

definition
  let M;
  func complvect(M) -> UnOp of setvect(M) means
:: MIDSP_1:def 15

  for W holds W + it.W = ID(M);
end;

definition
  let M;
  func zerovect(M) -> Element of setvect(M) equals
:: MIDSP_1:def 16
  ID(M);
end;

definition
  let M;
  func vectgroup(M) -> addLoopStr equals
:: MIDSP_1:def 17
  addLoopStr (# setvect(M), addvect(M),
    zerovect(M) #);
end;

registration
  let M;
  cluster vectgroup M -> strict non empty;
end;

theorem :: MIDSP_1:53
  the carrier of vectgroup(M) = setvect(M);

theorem :: MIDSP_1:54
  the addF of vectgroup(M) = addvect(M);

theorem :: MIDSP_1:55
  0.vectgroup(M) = zerovect M;

theorem :: MIDSP_1:56
  vectgroup(M) is add-associative right_zeroed right_complementable Abelian;