:: Atlas of Midpoint Algebra
:: by Micha{\l} Muzalewski
::
:: Received June 21, 1991
:: Copyright (c) 1991-2026 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;
definitions VECTSP_1;
theorems BINOP_1, MIDSP_1, RLVECT_1, VECTSP_1;
schemes BINOP_1;
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
x + x;
coherence;
end;
definition let M,G,w;
attr w is associating means
p@q = r iff w.(p,r) = w.(r,q);
end;
theorem Th1:
w is associating implies p@p = p
proof
A1: w.(p,p) = w.(p,p);
assume w is associating;
hence thesis by A1;
end;
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
(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
A1: w is_atlas_of S,G;
func (a,x).w -> Element of S means
:Def4:
w.(a,it) = x;
existence by A1;
uniqueness by A1;
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 Th2:
w is_atlas_of S,G implies w.(a,a) = 0.G
proof
assume w is_atlas_of S,G;
then w.(a,a) + w.(a,a) = w.(a,a);
hence thesis by RLVECT_1:9;
end;
theorem Th3:
w is_atlas_of S,G & w.(a,b) = 0.G implies a = b
proof
assume that
A1: w is_atlas_of S,G and
A2: w.(a,b) = 0.G;
w.(a,b) = w.(a,a) by A1,A2,Th2;
hence thesis by A1;
end;
theorem Th4:
w is_atlas_of S,G implies w.(a,b) = -w.(b,a)
proof
assume
A1: w is_atlas_of S,G;
then w.(b,a) + w.(a,b) = w.(b,b)
.= 0.G by A1,Th2;
then -w.(b,a) = --w.(a,b) by RLVECT_1:6;
hence thesis by RLVECT_1:17;
end;
theorem Th5:
w is_atlas_of S,G & w.(a,b) = w.(c,d) implies w.(b,a) = w.(d,c)
proof
assume that
A1: w is_atlas_of S,G and
A2: w.(a,b) = w.(c,d);
thus w.(b,a) = -w.(c,d) by A1,A2,Th4
.= w.(d,c) by A1,Th4;
end;
theorem Th6:
w is_atlas_of S,G implies for b,x ex a st w.(a,b) = x
proof
assume
A1: w is_atlas_of S,G;
let b,x;
consider a such that
A2: w.(b,a) = -x by A1;
take a;
w.(a,b) = -(-x) by A1,A2,Th4
.= x by RLVECT_1:17;
hence thesis;
end;
theorem Th7:
w is_atlas_of S,G & w.(b,a) = w.(c,a) implies b = c
proof
assume that
A1: w is_atlas_of S,G and
A2: w.(b,a) = w.(c,a);
w.(a,b) = w.(a,c) by A1,A2,Th5;
hence thesis by A1;
end;
theorem Th8:
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
proof
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
set r = p@q;
w.(p,r) = w.(r,q) by A2;
then w.(r,p) = w.(q,r) by A1,Th5;
hence thesis by A2;
end;
theorem Th9:
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
proof
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
consider r such that
A3: w.(r,q) = w.(q,p) by A1,Th6;
take r;
thus thesis by A2,A3;
end;
reserve G for add-associative right_zeroed right_complementable Abelian non
empty addLoopStr;
reserve x for Element of G;
theorem Th10:
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)
proof
let G be add-associative Abelian non empty addLoopStr, x,y,z,t be Element
of G;
thus (x+y)+(z+t) = x+(y+(z+t)) by RLVECT_1:def 3
.= x+(z+(y+t)) by RLVECT_1:def 3
.= (x+z)+(y+t) by RLVECT_1:def 3;
end;
theorem
for G being add-associative Abelian non empty addLoopStr, x,y being
Element of G holds Double (x + y) = Double x + Double y by Th10;
theorem Th12:
Double (-x) = -Double x
proof
0.G = Double 0.G by RLVECT_1:def 4
.= Double (x+-x) by RLVECT_1:def 10
.= Double x + Double (-x) by Th10;
hence thesis by RLVECT_1:6;
end;
theorem Th13:
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))
proof
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
let a,b,c,d be Point of M;
thus a@b = c@d implies w.(a,d) = w.(c,b)
proof
set p = a@b;
assume a@b = c@d;
then
A3: w.(c,p) = w.(p,d) by A2;
w.(a,p) = w.(p,b) by A2;
hence w.(a,d) = w.(c,p) + w.(p,b) by A1,A3
.= w.(c,b) by A1;
end;
thus w.(a,d) = w.(c,b) implies a@b = c@d
proof
set p = a@b;
assume
A4: w.(a,d) = w.(c,b);
w.(p,b) + w.(p,d) = w.(a,p) + w.(p,d) by A2
.= w.(a,d) by A1
.= w.(p,b) + w.(c,p) by A1,A4;
then w.(p,d) = w.(c,p) by RLVECT_1:8;
hence thesis by A2;
end;
end;
reserve w for Function of [:S,S:],the carrier of G;
theorem Th14:
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)
proof
assume
A1: w is_atlas_of S,G;
let a,b,b9,c,c9;
assume
A2: w.(a,b) = w.(b,c) & w.(a,b9) = w.(b9,c9);
thus w.(c,c9) = w.(c,b9) + w.(b9,c9) by A1
.= w.(c,a) + w.(a,b9) + w.(b9,c9) by A1
.= w.(c,b) + w.(b,a) + w.(a,b9) + w.(b9,c9) by A1
.= Double w.(b,a) + w.(a,b9) + w.(a,b9) by A1,A2,Th5
.= Double w.(b,a) + Double w.(a,b9) by RLVECT_1:def 3
.= Double (w.(b,a) + w.(a,b9)) by Th10
.= Double w.(b,b9) by A1;
end;
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;
coherence by MIDSP_1:56;
end;
theorem Th15:
(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
proof
set G = vectgroup(M);
thus for a being set holds a is Element of G iff a is Vector of M
proof
let a be set;
a is Element of G iff a is Element of setvect(M) by MIDSP_1:53;
hence thesis by MIDSP_1:48;
end;
thus 0.G = zerovect(M) by MIDSP_1:55
.= ID(M) by MIDSP_1:def 16;
thus for a,b being Element of G, x,y being Vector of M st a=x & b=y holds a+
b = x+y
proof
let a,b be Element of G,x,y be Vector of M such that
A1: a=x & b=y;
reconsider xx = x, yy = y as Element of setvect(M) by MIDSP_1:48;
thus a+b = (the addF of G).(a,b) by RLVECT_1:2
.= (addvect(M)).(xx,yy) by A1,MIDSP_1:54
.= xx+yy by MIDSP_1:def 14
.= x+y by MIDSP_1:def 13;
end;
end;
Lm1: (for a being Element of vectgroup(M) ex x being Element of vectgroup(M)
st Double x = a) & for a being Element of vectgroup(M) holds Double a = 0.
vectgroup(M) implies a = 0.vectgroup(M)
proof
set G = vectgroup(M);
set p = the Point of M;
thus for a being Element of G ex x being Element of G st Double x = a
proof
set p = the Point of M;
let a be Element of G;
reconsider aa = a as Vector of M by Th15;
consider q being Point of M such that
A1: aa = vect(p,q) by MIDSP_1:35;
set xx = vect(p,p@q);
reconsider x = xx as Element of G by Th15;
take x;
xx + xx = aa by A1,MIDSP_1:42;
hence thesis by Th15;
end;
let a be Element of G;
reconsider aa = a as Vector of M by Th15;
consider q being Point of M such that
A2: aa = vect(p,q) by MIDSP_1:35;
consider r being Point of M such that
A3: aa = vect(q,r) by MIDSP_1:35;
assume Double a = 0.G;
then aa + aa = 0.G by Th15
.= ID(M) by Th15;
then vect(p,q) + vect(q,r) = vect(p,p) by A2,A3,MIDSP_1:38;
then vect(p,r) = vect(p,p) by MIDSP_1:40;
then vect(p,q) = vect(q,p) by A2,A3,MIDSP_1:39;
then
A4: p@p = q@q by MIDSP_1:37;
p = p@p by MIDSP_1:def 3
.= q by A4,MIDSP_1:def 3;
hence a = ID(M) by A2,MIDSP_1:38
.= 0.G by Th15;
end;
definition
let IT be non empty addLoopStr;
attr IT is midpoint_operator means
:Def5:
(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;
coherence
proof
let L be non empty addLoopStr;
assume
A1: L is midpoint_operator;
let a be Element of L;
assume a + a = 0.L;
then Double a = 0.L;
hence thesis by A1;
end;
end;
registration
cluster strict midpoint_operator add-associative right_zeroed
right_complementable Abelian for non empty addLoopStr;
existence
proof
set M = the MidSp;
set G = vectgroup(M);
( for a being Element of G ex x being Element of G st Double x = a)&
for a being Element of G holds Double a = 0.G implies a = 0.G by Lm1;
then G is midpoint_operator;
hence thesis;
end;
end;
reserve G for midpoint_operator add-associative right_zeroed
right_complementable Abelian non empty addLoopStr;
reserve x,y for Element of G;
theorem Th16:
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
proof
let G be Fanoian add-associative right_zeroed right_complementable non
empty addLoopStr, x be Element of G;
A1: -x + x = 0.G by RLVECT_1:5;
assume x = -x;
hence thesis by A1,VECTSP_1:def 18;
end;
theorem Th17:
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
proof
let G be Fanoian add-associative right_zeroed right_complementable Abelian
non empty addLoopStr, x,y be Element of G;
assume Double x = Double y;
then 0.G = (x+x)+-(y+y) by RLVECT_1:def 10
.= x+x+(-y+-y) by RLVECT_1:31
.= x+(x+(-y+-y)) by RLVECT_1:def 3
.= x+(x+-y+-y) by RLVECT_1:def 3
.= (x+-y)+(x+-y) by RLVECT_1:def 3;
then -y+x = 0.G by VECTSP_1:def 18;
hence x = -(-y) by RLVECT_1:6
.= y by RLVECT_1:17;
end;
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
:Def6:
Double it = x;
existence by Def5;
uniqueness by Th17;
end;
theorem
Half 0.G = 0.G & Half (x+y) = Half x + Half y & (Half x = Half y
implies x = y) & Half Double x = x
proof
Double 0.G = 0.G by RLVECT_1:def 4;
hence Half 0.G = 0.G by Def6;
Double (Half x + Half y) = Double Half x + Double Half y by Th10
.= x + Double Half y by Def6
.= x + y by Def6;
hence Half (x+y) = Half x + Half y by Def6;
thus Half x = Half y implies x = y
proof
assume Half x = Half y;
hence x = Double Half y by Def6
.= y by Def6;
end;
thus thesis by Def6;
end;
theorem Th19:
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)
proof
let M be non empty MidStr, w be Function of [:the carrier of M,the carrier
of M:],the carrier of G;
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
let a,b,c,d be Point of M;
A3: w.(b,a@b) = w.(b,b@a) by A1,A2,Th8
.= w.(b@a,a) by A2
.= w.(a@b,a) by A1,A2,Th8;
set p = (a@b)@(c@d);
A4: w.(c,c@d) = w.(c@d,d) by A2;
A5: w.(b,b@d) = w.(b@d,d) by A2;
w.(c,a@c) = w.(c,c@a) by A1,A2,Th8
.= w.(c@a,a) by A2
.= w.(a@c,a) by A1,A2,Th8;
then Double w.(a@c,c@d) = w.(a,d) by A1,A4,Th14
.= -w.(d,a) by A1,Th4
.= -Double w.(b@d,a@b) by A1,A5,A3,Th14
.= Double -w.(b@d,a@b) by Th12
.= Double w.(a@b,b@d) by A1,Th4;
then w.(a@c,c@d) = w.(a@b,b@d) by Th17;
then
A6: w.(a@c,p) + w.(p,c@d) = w.(a@b,b@d) by A1
.= w.(p,b@d) + w.(a@b,p) by A1;
w.(a@b,p) = w.(p,c@d) by A2;
then w.(a@c,p) = w.(p,b@d) by A6,RLVECT_1:8;
hence thesis by A2;
end;
theorem Th20:
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
proof
let M be non empty MidStr, w be Function of [:the carrier of M,the carrier
of M:],the carrier of G;
assume w is_atlas_of the carrier of M,G & w is associating;
then
for a,b,c,d being Point of M holds a@a = a & a@b = b@a & (a@b)@(c@d) = (
a@c)@(b@d) & ex x being Point of M st x@a = b by Th1,Th8,Th9,Th19;
hence thesis by MIDSP_1:def 3;
end;
reserve x,y for Element of vectgroup(M);
registration
let M;
cluster vectgroup(M) -> midpoint_operator;
coherence
by Lm1;
end;
definition
let M,p,q;
func vector(p,q) -> Element of vectgroup(M) equals
vect(p,q);
coherence by Th15;
end;
definition
let M;
func vect(M) -> Function of [:the carrier of M,the carrier of M:], the
carrier of vectgroup(M) means
:Def8:
it.(p,q) = vect(p,q);
existence
proof
deffunc F(Point of M,Point of M) = vector($1,$2);
consider f being Function of [:the carrier of M,the carrier of M:], the
carrier of vectgroup(M) such that
A1: f.(p,q) = F(p,q) from BINOP_1:sch 4;
take f;
f.(p,q) = vect(p,q)
proof
thus f.(p,q) = vector(p,q) by A1
.= vect(p,q);
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:the carrier of M,the carrier of M:], the carrier
of vectgroup(M);
assume that
A2: f.(p,q) = vect(p,q) and
A3: g.(p,q) = vect(p,q);
f.(p,q) = g.(p,q)
proof
thus f.(p,q) = vect(p,q) by A2
.= g.(p,q) by A3;
end;
hence f = g by BINOP_1:2;
end;
end;
theorem Th21:
vect(M) is_atlas_of the carrier of M, vectgroup(M)
proof
set w = vect(M);
A1: ex q st w.(p,q) = x
proof
reconsider xx = x as Vector of M by Th15;
consider q such that
A2: xx = vect(p,q) by MIDSP_1:35;
take q;
thus thesis by A2,Def8;
end;
A3: w.(p,q) = w.(p,r) implies q = r
proof
assume w.(p,q) = w.(p,r);
then vect(p,q) = w.(p,r) by Def8
.= vect(p,r) by Def8;
hence thesis by MIDSP_1:39;
end;
w.(p,q) + w.(q,r) = w.(p,r)
proof
w.(p,q) = vect(p,q) & w.(q,r) = vect(q,r) by Def8;
hence w.(p,q) + w.(q,r) = vect(p,q) + vect(q,r) by Th15
.= vect(p,r) by MIDSP_1:40
.= w.(p,r) by Def8;
end;
hence thesis by A1,A3;
end;
theorem Th22:
vect(p,q) = vect(r,s) iff p@s = q@r
proof
thus vect(p,q) = vect(r,s) implies p@s = q@r by MIDSP_1:37;
thus p@s = q@r implies vect(p,q) = vect(r,s)
proof
assume p@s = q@r;
then p,q @@ r,s by MIDSP_1:def 4;
then [p,q] ## [r,s] by MIDSP_1:19;
hence thesis by MIDSP_1:36;
end;
end;
theorem Th23:
p@q = r iff vect(p,r) = vect(r,q)
proof
p@q = r iff p@q = r@r by MIDSP_1:def 3;
hence thesis by Th22;
end;
::$CT
Lm2: vect(M) is associating
proof
let p,q,r;
set w = vect(M);
w.(p,r) = vect(p,r) & w.(r,q) = vect(r,q) by Def8;
hence thesis by Th23;
end;
registration let M;
cluster vect M -> associating;
coherence by Lm2;
end;
:: Representation Theorem
reserve w for Function of [:S,S:],the carrier of G;
definition
let S,G,w;
assume
A1: w is_atlas_of S,G;
func @(w) -> BinOp of S means
:Def9:
w.(a,it.(a,b)) = w.(it.(a,b),b);
existence
proof
defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
$2);
A2: for a,b ex c st P[a,b,c]
proof
let a,b;
set x = Half w.(a,b);
consider c such that
A3: w.(a,c) = x by A1;
take c;
x + x = Double x .= w.(a,b) by Def6
.= x + w.(c,b) by A1,A3;
hence thesis by A3,RLVECT_1:8;
end;
consider o being BinOp of S such that
A4: for a,b holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A2);
take o;
thus thesis by A4;
end;
uniqueness
proof
defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
$2);
A5: for a,b,c,c9 st P[a,b,c] & P[a,b,c9] holds c = c9
proof
let a,b,c,c9 such that
A6: ( P[a,b,c])& P[a,b,c9];
w.(c,c9) = w.(c,a) + w.(a,c9) by A1
.= w.(c9,b) + w.(b,c) by A1,A6,Th5
.= w.(c9,c) by A1
.= -w.(c,c9) by A1,Th4;
then w.(c,c9) = 0.G by Th16;
hence thesis by A1,Th3;
end;
let f,g be BinOp of S such that
A7: ( for a,b holds w.(a,f.(a,b)) = w.(f.(a,b),b))& for a,b holds w.(a
,g.(a,b)) = w.(g.(a,b),b);
for a,b holds f.(a,b) = g.(a,b)
proof
let a,b;
w.(a,f.(a,b)) = w.(f.(a,b),b) & w.(a,g.(a,b)) = w.(g.(a,b),b) by A7;
hence thesis by A5;
end;
hence f = g by BINOP_1:2;
end;
end;
theorem Th24:
w is_atlas_of S,G implies for a,b,c holds @(w).(a,b) = c iff w.(
a,c) = w.(c,b)
proof
assume
A1: w is_atlas_of S,G;
let a,b,c;
thus @(w).(a,b) = c implies w.(a,c) = w.(c,b) by A1,Def9;
thus w.(a,c) = w.(c,b) implies @(w).(a,b) = c
proof
defpred P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,
$2);
assume
A2: w.(a,c) = w.(c,b);
A3: for a,b,c,c9 st P[a,b,c] & P[a,b,c9] holds c = c9
proof
let a,b,c,c9 such that
A4: ( P[a,b,c])& P[a,b,c9];
w.(c,c9) = w.(c,a) + w.(a,c9) by A1
.= w.(c9,b) + w.(b,c) by A1,A4,Th5
.= w.(c9,c) by A1
.= -w.(c,c9) by A1,Th4;
then w.(c,c9) = 0.G by Th16;
hence thesis by A1,Th3;
end;
set c9 = @(w).(a,b);
P[a,b,c9] by A1,Def9;
hence thesis by A2,A3;
end;
end;
registration
let D be non empty set, M be BinOp of D;
cluster MidStr(#D,M#) -> non empty;
coherence;
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
w;
coherence;
end;
theorem Th25:
w is_atlas_of S,G implies Atlas(w) is associating
proof
assume A1: w is_atlas_of S,G;
for a,b,c holds a@b = c iff (Atlas(w)).(a,c) = (Atlas(w)).(c,b)
proof
let a,b,c;
@(w).(a,b) = c iff w.(a,c) = w.(c,b) by A1,Th24;
hence thesis by MIDSP_1:def 1;
end;
hence thesis;
end;
definition
let S,G,w;
assume
A1: w is_atlas_of S,G;
func MidSp.w -> strict MidSp equals
MidStr (# S, @(w) #);
coherence
proof
set M = MidStr(#S,@(w)#), W = Atlas(w);
W is associating by A1,Th25;
hence thesis by A1,Th20;
end;
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 Th26:
M is MidSp iff ex G st ex w st w is_atlas_of the carrier of M,G
& w is associating
proof
hereby
assume
A1: M is MidSp;
thus ex G st ex w st w is_atlas_of the carrier of M,G &
w is associating
proof
reconsider M as MidSp by A1;
set G = vectgroup(M);
take G;
ex w being Function of [:the carrier of M,the carrier of M:], the
carrier of G st w is_atlas_of the carrier of M,G & w is associating
proof
take vect(M);
thus thesis by Th21;
end;
hence thesis;
end;
end;
given G being midpoint_operator add-associative right_zeroed
right_complementable Abelian non empty addLoopStr, w being Function of [:the
carrier of M,the carrier of M:],the carrier of G such that
A2: w is_atlas_of the carrier of M,G & w is associating;
thus thesis by A2,Th20;
end;
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
:Def12:
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;
existence
proof
consider G being midpoint_operator add-associative right_zeroed
right_complementable Abelian non empty addLoopStr, w being Function of [:the
carrier of M,the carrier of M:], the carrier of G such that
A1: w is_atlas_of the carrier of M,G & w is associating by Th26;
take AtlasStr(# G, w #);
thus thesis by A1;
end;
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
(the function of W).(a,b);
coherence;
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
(a,x).(the function of W);
coherence;
end;
definition
let M be MidSp, W be ATLAS of M;
func 0.W -> Vector of W equals
0.(the algebra of W);
coherence;
end;
theorem Th27:
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))
proof
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating;
A3: a@c = b1@b2 iff w.(a,b2) = w.(b1,c) by A1,A2,Th13;
hence a@c = b1@b2 implies w.(a,c) = w.(a,b1) + w.(a,b2) by A1;
w.(a,c) = w.(a,b1) + w.(b1,c) by A1;
hence thesis by A3,RLVECT_1:8;
end;
theorem Th28:
w is_atlas_of the carrier of M,G & w is associating
implies (a@c = b iff w.(a,c) = Double w.(a,b))
proof
assume
A1: w is_atlas_of the carrier of M,G & w is associating;
then reconsider MM = M as MidSp by Th20;
reconsider bb = b as Point of MM;
bb@bb = bb by MIDSP_1:def 3;
hence thesis by A1,Th27;
end;
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
a@c = b1@b2 iff W.(a,c) = W.(a,b1) + W.(a,b2)
proof
set w = the function of W, G = the algebra of W;
A1: G is midpoint_operator add-associative right_zeroed right_complementable
Abelian by Def12;
w is_atlas_of the carrier of M,G & w is associating by Def12;
hence thesis by A1,Th27;
end;
theorem
a@c = b iff W.(a,c) = Double W.(a,b)
proof
set w = the function of W, G = the algebra of W;
A1: G is midpoint_operator add-associative right_zeroed right_complementable
Abelian by Def12;
w is_atlas_of the carrier of M,G & w is associating by Def12;
hence thesis by A1,Th28;
end;
theorem
(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)
proof
set w = the function of W;
thus for a,x ex b st W.(a,b) = x
proof
set w = the function of W;
let a,x;
w is_atlas_of the carrier of M,(the algebra of W) by Def12;
then consider b such that
A1: w.(a,b) = x;
take b;
thus thesis by A1;
end;
thus for a,b,c holds W.(a,b) = W.(a,c) implies b = c
proof
set w = the function of W;
A2: w is_atlas_of (the carrier of M),(the algebra of W) by Def12;
let a,b,c;
assume W.(a,b) = W.(a,c);
hence thesis by A2;
end;
let a,b,c;
w is_atlas_of the carrier of M,(the algebra of W) by Def12;
hence thesis;
end;
theorem Th32:
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)
proof
set w = the function of W, G = the algebra of W;
A1: w is_atlas_of (the carrier of M),G by Def12;
A2: G is midpoint_operator add-associative right_zeroed right_complementable
Abelian by Def12;
hence W.(a,a) = 0.W by A1,Th2;
thus W.(a,b) = 0.W implies a = b by A2,A1,Th3;
thus W.(a,b) = -W.(b,a) by A2,A1,Th4;
thus W.(a,b) = W.(c,d) implies W.(b,a) = W.(d,c) by A2,A1,Th5;
thus for b,x ex a st W.(a,b) = x
proof
let b,x;
consider a such that
A3: w.(a,b) = x by A2,A1,Th6;
take a;
thus thesis by A3;
end;
thus W.(b,a) = W.(c,a) implies b = c by A2,A1,Th7;
A4: w is associating by Def12;
hence a@b = c iff W.(a,c) = W.(c,b);
thus a@b = c@d iff W.(a,d) = W.(c,b) by A2,A4,A1,Th13;
thus thesis by A1,Def4;
end;
theorem
(a,0.W).W = a
proof
W.(a,a) = 0.W by Th32;
hence thesis by Th32;
end;