Copyright (c) 1991 Association of Mizar Users
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;
definitions STRUCT_0, VECTSP_1;
theorems BINOP_1, MIDSP_1, RLVECT_1, VECTSP_1;
schemes BINOP_1, FUNCT_2;
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
:Def1: x + x;
coherence;
end;
definition let M,G,w;
pred M,G are_associated_wrp w means
:Def2: p@q = r iff w.(p,r) = w.(r,q);
end;
theorem
Th1: M,G are_associated_wrp w implies p@p = p
proof
assume A1: M,G are_associated_wrp w;
w.(p,p) = w.(p,p);
hence p@p = p by A1,Def2;
end;
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
:Def3: (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,Def3;
uniqueness by A1,Def3;
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
Th2: Double 0.G = 0.G
proof
thus Double 0.G = 0.G + 0.G by Def1
.= 0.G by RLVECT_1:def 7;
end;
canceled;
theorem
Th4: 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) by Def3;
hence thesis by RLVECT_1:22;
end;
theorem
Th5: 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,Th4;
hence thesis by A1,Def3;
end;
theorem
Th6: 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) by Def3
.= 0.G by A1,Th4;
then -w.(b,a) = --w.(a,b) by RLVECT_1:19;
hence thesis by RLVECT_1:30;
end;
theorem
Th7: 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,Th6
.= w.(d,c) by A1,Th6;
end;
theorem
Th8: 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,Def3;
A3: w.(a,b) = -(-x) by A1,A2,Th6
.= x by RLVECT_1:30;
take a;
thus thesis by A3;
end;
theorem
Th9: 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,Th7;
hence thesis by A1,Def3;
end;
theorem
Th10: 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
proof
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume
A1: w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;
set r = p@q;
w.(p,r) = w.(r,q) by A1,Def2;
then w.(r,p) = w.(q,r) by A1,Th7;
hence p@q = q@p by A1,Def2;
end;
theorem
Th11: 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
proof
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume
A1: w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;
then consider r such that
A2: w.(r,q) = w.(q,p) by Th8;
take r;
thus thesis by A1,A2,Def2;
end;
reserve G for add-associative right_zeroed right_complementable
Abelian (non empty LoopStr);
reserve x for Element of G;
canceled;
theorem Th13:
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)
proof
let G be add-associative Abelian (non empty LoopStr),
x,y,z,t be Element of G;
thus (x+y)+(z+t) = x+(y+(z+t)) by RLVECT_1:def 6
.= x+(z+(y+t)) by RLVECT_1:def 6
.= (x+z)+(y+t) by RLVECT_1:def 6;
end;
theorem Th14:
for G being add-associative Abelian (non empty LoopStr),
x,y being Element of G holds
Double (x + y) = Double x + Double y
proof
let G be add-associative Abelian (non empty LoopStr),
x,y be Element of G;
thus Double (x + y) = (x + y) + (x + y) by Def1
.= (x + x) + (y + y) by Th13
.= Double x + (y + y) by Def1
.= Double x + Double y by Def1;
end;
theorem
Th15: Double (-x) = -Double x
proof
0.G = Double 0.G by Th2
.= Double (x+-x) by RLVECT_1:def 10
.= Double x + Double (-x) by Th14;
hence thesis by RLVECT_1:19;
end;
theorem
Th16: 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))
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: M,G are_associated_wrp w;
let a,b,c,d be Point of M;
thus a@b = c@d implies w.(a,d) = w.(c,b)
proof
assume A3: a@b = c@d;
set p = a@b;
w.(a,p) = w.(p,b) & w.(c,p) = w.(p,d) by A2,A3,Def2;
hence w.(a,d) = w.(c,p) + w.(p,b) by A1,Def3
.= w.(c,b) by A1,Def3;
end;
thus w.(a,d) = w.(c,b) implies a@b = c@d
proof
assume A4: w.(a,d) = w.(c,b);
set p = a@b;
w.(p,b) + w.(p,d) = w.(a,p) + w.(p,d) by A2,Def2
.= w.(a,d) by A1,Def3
.= w.(p,b) + w.(c,p) by A1,A4,Def3;
then w.(p,d) = w.(c,p) by RLVECT_1:21;
hence a@b = c@d by A2,Def2;
end;
end;
reserve w for Function of [:S,S:],the carrier of G;
theorem
Th17: 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')
proof
assume A1: w is_atlas_of S,G;
let a,b,b',c,c';
assume A2: w.(a,b) = w.(b,c) & w.(a,b') = w.(b',c');
thus w.(c,c') = w.(c,b') + w.(b',c') by A1,Def3
.= w.(c,a) + w.(a,b') + w.(b',c') by A1,Def3
.= w.(c,b) + w.(b,a) + w.(a,b') + w.(b',c') by A1,Def3
.= w.(b,a) + w.(b,a) + w.(a,b') + w.(a,b') by A1,A2,Th7
.= Double w.(b,a) + w.(a,b') + w.(a,b') by Def1
.= Double w.(b,a) + (w.(a,b') + w.(a,b')) by RLVECT_1:def 6
.= Double w.(b,a) + Double w.(a,b') by Def1
.= Double (w.(b,a) + w.(a,b')) by Th14
.= Double w.(b,b') by A1,Def3;
end;
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;
coherence by MIDSP_1:86;
end;
theorem
Th18: (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:82;
hence thesis by MIDSP_1:71;
end;
thus 0.G = the Zero of G by RLVECT_1:def 2
.= zerovect(M) by MIDSP_1:85
.= ID(M) by MIDSP_1:def 17;
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:71;
thus a+b = (the add of G).(a,b) by RLVECT_1:5
.= (addvect(M)).(xx,yy) by A1,MIDSP_1:83
.= xx+yy by MIDSP_1:def 15
.= x+y by MIDSP_1:def 14;
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);
thus for a being Element of G
ex x being Element of G st Double x = a
proof
let a be Element of G;
reconsider aa = a as Vector of M by Th18;
consider p being Point of M;
consider q being Point of M such that
A1: aa = vect(p,q) by MIDSP_1:55;
set xx = vect(p,p@q);
A2: xx + xx = aa by A1,MIDSP_1:62;
reconsider x = xx as Element of G by Th18;
A3: x + x = a by A2,Th18;
take x;
thus thesis by A3,Def1;
end;
let a be Element of G;
assume Double a = 0.G;
then A4: a + a = 0.G by Def1;
reconsider aa = a as Vector of M by Th18;
consider p being Point of M;
consider q being Point of M such that
A5: aa = vect(p,q) by MIDSP_1:55;
A6: aa + aa = 0.G by A4,Th18
.= ID(M) by Th18;
consider r being Point of M such that
A7: aa = vect(q,r) by MIDSP_1:55;
vect(p,q) + vect(q,r) = vect(p,p) by A5,A6,A7,MIDSP_1:58;
then vect(p,r) = vect(p,p) by MIDSP_1:60;
then vect(p,q) = vect(q,p) by A5,A7,MIDSP_1:59;
then A8: p@p = q@q by MIDSP_1:57;
p = p@p by MIDSP_1:def 4
.= q by A8,MIDSP_1:def 4;
hence a = ID(M) by A5,MIDSP_1:58
.= 0.G by Th18;
end;
definition let IT be non empty LoopStr;
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;
definition
cluster midpoint_operator -> Fanoian (non empty LoopStr);
coherence
proof
let L be non empty LoopStr;
assume A1: L is midpoint_operator;
let a be Element of L; assume a + a = 0.L;
then Double a = 0.L by Def1;
hence thesis by A1,Def5;
end;
end;
definition
cluster strict midpoint_operator add-associative right_zeroed
right_complementable Abelian (non empty LoopStr);
existence
proof
consider M;
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 by Def5;
hence thesis;
end;
end;
reserve G for midpoint_operator add-associative right_zeroed
right_complementable Abelian (non empty LoopStr);
reserve x,y for Element of G;
theorem Th19:
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
proof
let G be Fanoian add-associative right_zeroed right_complementable
(non empty LoopStr),
x be Element of G;
assume A1:x = -x;
-x + x = 0.G by RLVECT_1:16;
hence thesis by A1,VECTSP_1:def 28;
end;
theorem Th20:
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
proof
let G be Fanoian add-associative right_zeroed
right_complementable Abelian (non empty LoopStr),
x,y be Element of G;
assume Double x = Double y;
then x+x = Double y by Def1;
then (x+x)+-(y+y) = (y+y)+-(y+y) by Def1;
then 0.G = (x+x)+-(y+y) by RLVECT_1:def 10
.= x+x+(-y+-y) by RLVECT_1:45
.= x+(x+(-y+-y)) by RLVECT_1:def 6
.= x+(x+-y+-y) by RLVECT_1:def 6
.= (x+-y)+(x+-y) by RLVECT_1:def 6;
then -y+x = 0.G by VECTSP_1:def 28;
hence x = -(-y) by RLVECT_1:19
.= y by RLVECT_1:30;
end;
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
:Def6: Double it = x;
existence by Def5;
uniqueness by Th20;
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 Th2;
hence Half 0.G = 0.G by Def6;
Double (Half x + Half y) = Double Half x + Double Half y by Th14
.= 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 Half Double x = x by Def6;
end;
theorem
Th22: 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)
proof
let M be non empty MidStr,
w be Function of [:the carrier of M,the carrier of M:],the carrier of G;
assume A1: w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;
let a,b,c,d be Point of M;
set p = (a@b)@(c@d);
A2: w.(a@b,p) = w.(p,c@d) by A1,Def2;
A3: w.(c,a@c) = w.(c,c@a) by A1,Th10
.= w.(c@a,a) by A1,Def2
.= w.(a@c,a) by A1,Th10;
A4: w.(c,c@d) = w.(c@d,d) by A1,Def2;
A5: w.(b,b@d) = w.(b@d,d) by A1,Def2;
A6: w.(b,a@b) = w.(b,b@a) by A1,Th10
.= w.(b@a,a) by A1,Def2
.= w.(a@b,a) by A1,Th10;
Double w.(a@c,c@d) = w.(a,d) by A1,A3,A4,Th17
.= -w.(d,a) by A1,Th6
.= -Double w.(b@d,a@b) by A1,A5,A6,Th17
.= Double -w.(b@d,a@b) by Th15
.= Double w.(a@b,b@d) by A1,Th6;
then w.(a@c,c@d) = w.(a@b,b@d) by Th20;
then w.(a@c,p) + w.(p,c@d) = w.(a@b,b@d) by A1,Def3
.= w.(p,b@d) + w.(a@b,p) by A1,Def3;
then w.(a@c,p) = w.(p,b@d) by A2,RLVECT_1:21;
hence p = (a@c)@(b@d) by A1,Def2;
end;
theorem
Th23: 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
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: M,G are_associated_wrp w;
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 A1,A2,Th1,Th10,Th11,Th22;
hence thesis by MIDSP_1:def 4;
end;
reserve x,y for Element of vectgroup(M);
definition let M;
cluster vectgroup(M) -> midpoint_operator;
coherence
proof
set G = vectgroup(M);
(for x ex y st Double y = x) & for x holds Double
x = 0.G implies x = 0.G by Lm1;
hence thesis by Def5;
end;
end;
definition let M,p,q;
func vector(p,q) -> Element of vectgroup(M) equals
:Def7: vect(p,q);
coherence by Th18;
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 Lambda2D;
A2: f.(p,q) = vect(p,q)
proof
f.[p,q] = vector(p,q) by A1
.= vect(p,q) by Def7;
hence thesis by BINOP_1:def 1;
end;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of [:the carrier of M,the carrier of M:],
the carrier of vectgroup(M);
assume that
A3: f.(p,q) = vect(p,q) and
A4: g.(p,q) = vect(p,q);
f.(p,q) = g.(p,q)
proof
thus f.(p,q) = vect(p,q) by A3
.= g.(p,q) by A4;
end;
hence f = g by BINOP_1:2;
end;
end;
theorem
Th24: 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 Th18;
consider q such that
A2: xx = vect(p,q) by MIDSP_1:55;
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:59;
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 Th18
.= vect(p,r) by MIDSP_1:60
.= w.(p,r) by Def8;
end;
hence thesis by A1,A3,Def3;
end;
theorem
Th25: 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:57;
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 5;
then [p,q] ## [r,s] by MIDSP_1:31;
hence thesis by MIDSP_1:56;
end;
end;
theorem
Th26: p@q = r iff vect(p,r) = vect(r,q)
proof
p@q = r iff p@q = r@r by MIDSP_1:def 4;
hence thesis by Th25;
end;
theorem
Th27: M,vectgroup(M) are_associated_wrp vect(M)
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 Th26;
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,Def3;
A4: x + x = Double x by Def1
.= w.(a,b) by Def6
.= x + w.(c,b) by A1,A3,Def3;
take c;
thus thesis by A3,A4,RLVECT_1:21;
end;
consider o being BinOp of S such that
A5: for a,b holds P[a,b,o.(a,b)] from BinOpEx(A2);
take o;
thus thesis by A5;
end;
uniqueness
proof
let f,g be BinOp of S such that
A6: for a,b holds w.(a,f.(a,b)) = w.(f.(a,b),b) and
A7: for a,b holds w.(a,g.(a,b)) = w.(g.(a,b),b);
defpred
P[Element of S,Element of S,Element of S] means w.($1,$3) = w.($3,$2);
A8: for a,b,c,c' st P[a,b,c] & P[a,b,c'] holds c = c'
proof
let a,b,c,c' such that
A9: P[a,b,c] and
A10: P[a,b,c'];
w.(c,c') = w.(c,a) + w.(a,c') by A1,Def3
.= w.(c',b) + w.(b,c) by A1,A9,A10,Th7
.= w.(c',c) by A1,Def3
.= -w.(c,c') by A1,Th6;
then w.(c,c') = 0.G by Th19;
hence thesis by A1,Th5;
end;
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 A6,A7
;
hence thesis by A8;
end;
hence f = g by BINOP_1:2;
end;
end;
theorem
Th28: 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
assume A2: w.(a,c) = w.(c,b);
defpred P[Element of S,Element of S,Element of S] means
w.($1,$3) = w.($3,$2);
A3: for a,b,c,c' st P[a,b,c] & P[a,b,c'] holds c = c'
proof
let a,b,c,c' such that
A4: P[a,b,c] and
A5: P[a,b,c'];
w.(c,c') = w.(c,a) + w.(a,c') by A1,Def3
.= w.(c',b) + w.(b,c) by A1,A4,A5,Th7
.= w.(c',c) by A1,Def3
.= -w.(c,c') by A1,Th6;
then w.(c,c') = 0.G by Th19;
hence thesis by A1,Th5;
end;
set c' = @(w).(a,b);
P[a,b,c'] by A1,Def9;
hence c = c' by A2,A3;
end;
end;
definition let D be non empty set, M be BinOp of D;
cluster MidStr(#D,M#) -> non empty;
coherence
proof
thus the carrier of MidStr(#D,M#) is non empty;
end;
end;
reserve a,b,c for Point of MidStr(#S,@(w)#);
Lm2: @(w).(a,b) = a@b
proof
thus thesis by MIDSP_1:def 1;
end;
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
:Def10: w;
coherence;
end;
Lm3: w is_atlas_of S,G implies for a,b,c holds
a@b = c iff (Atlas(w)).(a,c) = (Atlas(w)).(c,b)
proof
assume A1: w is_atlas_of S,G;
let a,b,c;
set W = (Atlas(w));
A2: W.(a,c) = w.(a,c) & W.(c,b) = w.(c,b) by Def10;
@(w).(a,b) = c iff w.(a,c) = w.(c,b) by A1,Th28;
hence thesis by A2,Lm2;
end;
canceled 3;
theorem
Th32: w is_atlas_of S,G implies MidStr(#S,@(w)#),G are_associated_wrp Atlas(w)
proof
assume w is_atlas_of S,G;
then for a,b,c holds a@b = c iff (Atlas(w)).(a,c) = (Atlas(w)).(c,b) by Lm3
;
hence thesis by Def2;
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);
A2: W is_atlas_of the carrier of M,G by A1,Def10;
M,G are_associated_wrp W by A1,Th32;
hence M is strict MidSp by A2,Th23;
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
Th33: 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
proof
hereby assume A1: M is MidSp;
thus ex G st ex w
st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w
proof
reconsider M as MidSp by A1;
set G = vectgroup(M);
A2: 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 & M,G are_associated_wrp w
proof
take vect(M);
thus thesis by Th24,Th27;
end;
take G;
thus thesis by A2;
end;
end;
given G being midpoint_operator
add-associative right_zeroed right_complementable
Abelian (non empty LoopStr), w being Function of
[:the carrier of M,the carrier of M:],the carrier of G such that
A3: w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;
thus M is MidSp by A3,Th23;
end;
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 :Def12:
the algebra of IT is midpoint_operator
add-associative right_zeroed right_complementable Abelian &
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;
existence
proof
consider G being midpoint_operator
add-associative right_zeroed right_complementable Abelian
(non empty LoopStr),
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 and
A2: M,G are_associated_wrp w by Th33;
take AtlasStr(# G, w #);
thus thesis by A1,A2,Def12;
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
:Def13: (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
:Def14: (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
:Def15: 0.(the algebra of W);
coherence;
end;
:: SOME USEFUL PROPOSITIONS
theorem Th34:
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))
proof
assume that
A1: w is_atlas_of the carrier of M,G and
A2: M,G are_associated_wrp w;
A3: a@c = b1@b2 iff w.(a,b2) = w.(b1,c) by A1,A2,Th16;
A4: w.(a,c) = w.(a,b1) + w.(b1,c) by A1,Def3;
thus a@c = b1@b2 implies w.(a,c) = w.(a,b1) + w.(a,b2) by A1,A3,Def3;
thus w.(a,c) = w.(a,b1) + w.(a,b2) implies a@c = b1@b2
by A3,A4,RLVECT_1:21;
end;
theorem
Th35: 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))
proof
assume
A1: w is_atlas_of the carrier of M,G & M,G are_associated_wrp w;
then reconsider MM = M as MidSp by Th23;
reconsider bb = b as Point of MM;
A2: bb@bb = bb by MIDSP_1:def 4;
a@c = b@b iff w.(a,c) = w.(a,b) + w.(a,b) by A1,Th34;
hence thesis by A2,Def1;
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: w is_atlas_of the carrier of M,G by Def12;
A2: M,G are_associated_wrp w by Def12;
A3: G is midpoint_operator
add-associative right_zeroed right_complementable Abelian by Def12;
W.(a,c) = w.(a,c) & W.(a,b1) = w.(a,b1) & W.(a,b2) = w.(a,b2) by Def13;
hence thesis by A1,A2,A3,Th34;
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: w is_atlas_of the carrier of M,G by Def12;
A2: M,G are_associated_wrp w by Def12;
A3: G is midpoint_operator
add-associative right_zeroed right_complementable Abelian by Def12;
W.(a,c) = w.(a,c) & W.(a,b) = w.(a,b) by Def13;
hence thesis by A1,A2,A3,Th35;
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
thus for a,x ex b st W.(a,b) = x
proof
let a,x;
set w = the function of W;
w is_atlas_of the carrier of M,(the algebra of W) by Def12;
then consider b such that
A1: w.(a,b) = x by Def3;
take b;
thus thesis by A1,Def13;
end;
thus for a,b,c holds W.(a,b) = W.(a,c) implies b = c
proof
let a,b,c such that
A2: W.(a,b) = W.(a,c);
set w = the function of W;
A3: W.(a,b) = w.(a,b) & W.(a,c) = w.(a,c) by Def13;
w is_atlas_of (the carrier of M),(the algebra of W) by Def12;
hence thesis by A2,A3,Def3;
end;
let a,b,c;
set w = the function of W;
A4: W.(a,b) = w.(a,b) & W.(b,c) = w.(b,c) & W.(a,c) = w.(a,c)
by Def13;
w is_atlas_of the carrier of M,(the algebra of W) by Def12;
hence thesis by A4,Def3;
end;
theorem
Th39: 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: G is midpoint_operator
add-associative right_zeroed right_complementable Abelian by Def12;
A2: M,G are_associated_wrp w & w is_atlas_of (the carrier of M),G
by Def12;
A3: W.(a,a) = w.(a,a) & W.(a,b) = w.(a,b) & W.(b,a) = w.(b,a)
& W.(c,d) = w.(c,d) & W.(d,c) = w.(d,c) & W.(c,a) = w.(c,a)
& W.(a,c) = w.(a,c) & W.(c,b) = w.(c,b) & W.(a,d) = w.(a,d)
& (a,x).W = (a,x).w by Def13,Def14;
A4: 0.W = 0.G by Def15;
hence W.(a,a) = 0.W by A1,A2,A3,Th4;
thus W.(a,b) = 0.W implies a = b by A1,A2,A3,A4,Th5;
thus W.(a,b) = -W.(b,a) by A1,A2,A3,Th6;
thus W.(a,b) = W.(c,d) implies W.(b,a) = W.(d,c) by A1,A2,A3,Th7;
thus for b,x ex a st W.(a,b) = x
proof
let b,x;
consider a such that
A5: w.(a,b) = x by A1,A2,Th8;
take a;
thus thesis by A5,Def13;
end;
thus W.(b,a) = W.(c,a) implies b = c by A1,A2,A3,Th9;
thus a@b = c iff W.(a,c) = W.(c,b) by A2,A3,Def2;
thus a@b = c@d iff W.(a,d) = W.(c,b) by A1,A2,A3,Th16;
thus thesis by A2,A3,Def4;
end;
theorem
(a,0.W).W = a
proof
W.(a,a) = 0.W by Th39;
hence thesis by Th39;
end;