The abstract of the Mizar article:

Midpoint algebras

by

Michal Muzalewski

Received November 26, 1989

MML identifier: MIDSP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BINOP_1, QC_LANG1, FUNCT_1, BOOLE, MCART_1, RELAT_1, VECTSP_1,
      ARYTM_1, RLVECT_1, MIDSP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, STRUCT_0, RLVECT_1,
      MCART_1, FUNCT_1, FUNCT_2;
 constructors BINOP_1, VECTSP_1, MCART_1, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: PRELIMINARY

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

definition
 cluster non empty 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 op2 -> BinOp of {{}} means
:: MIDSP_1:def 2
not contradiction;
end;

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

definition
 cluster Example -> strict non empty;
end;

canceled 4;

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

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

theorem :: MIDSP_1:7
    for a being Element of Example holds a = {};

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

canceled;

theorem :: MIDSP_1:10
 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 4
  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;

definition
 cluster strict MidSp-like (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,a',b',c',d',x,y,x' for Element of M;

canceled 4;

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

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

theorem :: MIDSP_1:17
 a@b = a implies a = b;

theorem :: MIDSP_1:18
 x@a = x'@a implies x = x';

theorem :: MIDSP_1:19
  a@x = a@x' implies x = x';
:: left-cancellation-law

:: B. CONGRUENCE RELATION

definition
  let M,a,b,c,d;
  pred a,b @@ c,d :: bound-vectors ab, cd are equivallent
  means
:: MIDSP_1:def 5
 a@d = b@c;
end;

canceled;

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

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

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

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

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

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

theorem :: MIDSP_1:27
 a,b @@ c,d & a,b @@ c,d' implies d = d';

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

theorem :: MIDSP_1:29
 a,b @@ a',b' & b,c @@ b',c' implies a,c @@ a',c';

:: C. BOUND-VECTORS

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

definition
 let M,p;
 redefine func p`1 -> Element of M;
end;

definition
 let M,p;
 redefine func p`2 -> Element of M;
end;

definition let M,p,q;
  pred p ## q means
:: MIDSP_1:def 6
p`1,p`2 @@ q`1,q`2;
  reflexivity;
  symmetry;
end;

definition let M,a,b;
 redefine func [a,b] -> Element of [:the carrier of M,the carrier of M:];
end;

canceled;

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

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

canceled 2;

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

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

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

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

theorem :: MIDSP_1:39
 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 7
     { q : q ## p};
end;

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

canceled;

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

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

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

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

theorem :: MIDSP_1:45
   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 8
ex p st it = p~;
end;

reserve u,v,w,u',w' for Vector of M;

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

canceled 2;

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

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

canceled;

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

theorem :: MIDSP_1:51
  ex w,p,q st u = p~ & v = q~ & p`2 = q`1 & w = [p`1,q`2]~;

theorem :: MIDSP_1:52
 (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 & w' = [p`1,q`2]~)
      implies w = w';

definition
  let M,u,v;
  func u + v -> Vector of M means
:: MIDSP_1:def 10
  ex p,q st (u = p~ & v = q~ & p`2 = q`1 & it = [p`1,q`2]~);
end;

:: E. ATLAS

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

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

canceled;

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

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

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

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

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

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

:: F. VECTOR GROUPS

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

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

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

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

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

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

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

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

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

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

reserve x for set;

canceled 3;

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

definition 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 14
  for u,v holds u1 = u & v1 = v implies it = u + v;
end;

canceled 2;

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

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

definition let M;
 func addvect(M) -> BinOp of setvect(M) means
:: MIDSP_1:def 15
  for u1,v1 holds it.(u1,v1) = u1 + v1;
end;

canceled;

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

theorem :: MIDSP_1:78
 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 16
  for W holds W + it.W = ID(M);
end;

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

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

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

canceled 3;

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

theorem :: MIDSP_1:83
the add of vectgroup(M) = addvect(M);

canceled;

theorem :: MIDSP_1:85
the Zero of vectgroup(M) = zerovect(M);

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