Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Midpoint algebras

by
Michal Muzalewski

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