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