Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Atlas of Midpoint Algebra

by
Michal Muzalewski

MML identifier: MIDSP_2
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, MIDSP_1, PRE_TOPC, FUNCT_1, QC_LANG1, ARYTM_1, VECTSP_1,
RLVECT_2, BINOP_1, MIDSP_2;
notation XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, BINOP_1, STRUCT_0, PRE_TOPC,
RLVECT_1, VECTSP_1, MIDSP_1;
constructors BINOP_1, MIDSP_1, VECTSP_1, MEMBERED, XBOOLE_0;
clusters MIDSP_1, STRUCT_0, RELSET_1, SUBSET_1, VECTSP_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin

::
:: GROUP OF FREE VECTORS
::

reserve G for non empty LoopStr;
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;
pred M,G are_associated_wrp w means
:: MIDSP_2:def 2
p@q = r iff w.(p,r) = w.(r,q);
end;

theorem :: MIDSP_2:1
M,G are_associated_wrp w implies p@p = p;

reserve S for non empty set;
reserve a,b,b',c,c',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 LoopStr);
reserve x for Element of G;
reserve w for Function of [:S,S:],the carrier of G;

theorem :: MIDSP_2:2
Double 0.G = 0.G;

canceled;

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

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

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

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

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

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

theorem :: MIDSP_2:10
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 & M,G are_associated_wrp w
implies p@q = q@p;

theorem :: MIDSP_2:11
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 & M,G are_associated_wrp w
implies ex r st r@p = q;

reserve G for add-associative right_zeroed right_complementable
Abelian (non empty LoopStr);
reserve x for Element of G;

canceled;

theorem :: MIDSP_2:13
for G being add-associative Abelian (non empty LoopStr),
x,y,z,t being Element of G holds
(x+y)+(z+t) = (x+z)+(y+t);

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

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

theorem :: MIDSP_2:16
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 & M,G are_associated_wrp w 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:17
w is_atlas_of S,G implies for a,b,b',c,c' holds
w.(a,b) = w.(b,c) & w.(a,b') = w.(b',c') implies w.(c,c') = Double w.(b,b');

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

definition let M;
cluster vectgroup(M) -> Abelian add-associative right_zeroed
right_complementable;
end;

theorem :: MIDSP_2:18
(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 LoopStr;
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;

definition
cluster midpoint_operator -> Fanoian (non empty LoopStr);
end;

definition
right_complementable Abelian (non empty LoopStr);
end;

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

theorem :: MIDSP_2:19
for G being Fanoian add-associative right_zeroed
right_complementable (non empty LoopStr),
x being Element of G holds
x = -x implies x = 0.G;

theorem :: MIDSP_2:20
for G being Fanoian add-associative right_zeroed
right_complementable Abelian (non empty LoopStr),
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 LoopStr),
x be Element of G;
func Half x -> Element of G means
:: MIDSP_2:def 6
Double it = x;
end;

theorem :: MIDSP_2:21
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:22
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 & M,G are_associated_wrp w
implies for a,b,c,d being Point of M holds
(a@b)@(c@d) = (a@c)@(b@d);

theorem :: MIDSP_2:23
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 & M,G are_associated_wrp w
implies M is MidSp;

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

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

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

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

theorem :: MIDSP_2:27
M,vectgroup(M) are_associated_wrp vect(M);

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

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

canceled 3;

theorem :: MIDSP_2:32
w is_atlas_of S,G implies MidStr(#S,@(w)#),G are_associated_wrp Atlas(w);

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

definition let M be non empty MidStr;
struct AtlasStr over M
(# algebra -> non empty LoopStr,
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
M,the algebra of IT are_associated_wrp the function of IT
& the function of IT is_atlas_of the carrier of M,the algebra of IT;
end;

definition let M be MidSp;
cluster ATLAS-like 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;

:: SOME USEFUL PROPOSITIONS

theorem :: MIDSP_2:34
w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
implies (a@c = b1@b2 iff w.(a,c) = w.(a,b1) + w.(a,b2));

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

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

theorem :: MIDSP_2:38
(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:39
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:40
(a,0.W).W = a;
```