begin
definition
let S be non
empty set ;
let G be non
empty addLoopStr ;
let w be
Function of
[:S,S:], the
carrier of
G;
pred w is_atlas_of S,
G means :
Def3:
( ( for
a being
Element of
S for
x being
Element of
G ex
b being
Element of
S st
w . (
a,
b)
= x ) & ( for
a,
b,
c being
Element of
S st
w . (
a,
b)
= w . (
a,
c) holds
b = c ) & ( for
a,
b,
c being
Element of
S holds
(w . (a,b)) + (w . (b,c)) = w . (
a,
c) ) );
end;
::
deftheorem Def3 defines
is_atlas_of MIDSP_2:def 3 :
for S being non empty set
for G being non empty addLoopStr
for w being Function of [:S,S:], the carrier of G holds
( w is_atlas_of S,G iff ( ( for a being Element of S
for x being Element of G ex b being Element of S st w . (a,b) = x ) & ( for a, b, c being Element of S st w . (a,b) = w . (a,c) holds
b = c ) & ( for a, b, c being Element of S holds (w . (a,b)) + (w . (b,c)) = w . (a,c) ) ) );
theorem Th5:
for
S being non
empty set for
a,
b,
c,
d being
Element of
S for
G being non
empty right_complementable add-associative right_zeroed addLoopStr for
w being
Function of
[:S,S:], the
carrier of
G st
w is_atlas_of S,
G &
w . (
a,
b)
= w . (
c,
d) holds
w . (
b,
a)
= w . (
d,
c)
theorem Th14:
for
S being non
empty set for
G being non
empty right_complementable Abelian add-associative right_zeroed addLoopStr for
w being
Function of
[:S,S:], the
carrier of
G st
w is_atlas_of S,
G holds
for
a,
b,
b9,
c,
c9 being
Element of
S st
w . (
a,
b)
= w . (
b,
c) &
w . (
a,
b9)
= w . (
b9,
c9) holds
w . (
c,
c9)
= Double (w . (b,b9))
Lm1:
for M being MidSp holds
( ( 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) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M) ) )
definition
let M be
MidSp;
existence
ex b1 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
for p, q being Point of M holds b1 . (p,q) = vect (p,q)
uniqueness
for b1, b2 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st ( for p, q being Point of M holds b1 . (p,q) = vect (p,q) ) & ( for p, q being Point of M holds b2 . (p,q) = vect (p,q) ) holds
b1 = b2
end;
Lm2:
for M being MidSp holds vect M is associating
definition
let S be non
empty set ;
let G be non
empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let w be
Function of
[:S,S:], the
carrier of
G;
assume A1:
w is_atlas_of S,
G
;
func @ w -> BinOp of
S means :
Def9:
for
a,
b being
Element of
S holds
w . (
a,
(it . (a,b)))
= w . (
(it . (a,b)),
b);
existence
ex b1 being BinOp of S st
for a, b being Element of S holds w . (a,(b1 . (a,b))) = w . ((b1 . (a,b)),b)
uniqueness
for b1, b2 being BinOp of S st ( for a, b being Element of S holds w . (a,(b1 . (a,b))) = w . ((b1 . (a,b)),b) ) & ( for a, b being Element of S holds w . (a,(b2 . (a,b))) = w . ((b2 . (a,b)),b) ) holds
b1 = b2
end;
theorem
for
M being
MidSp for
W being
ATLAS of
M for
a,
c,
b1,
b2 being
Point of
M holds
(
a @ c = b1 @ b2 iff
W . (
a,
c)
= (W . (a,b1)) + (W . (a,b2)) )
theorem
for
M being
MidSp for
W being
ATLAS of
M holds
( ( for
a being
Point of
M for
x being
Vector of
W ex
b being
Point of
M st
W . (
a,
b)
= x ) & ( for
a,
b,
c being
Point of
M st
W . (
a,
b)
= W . (
a,
c) holds
b = c ) & ( for
a,
b,
c being
Point of
M holds
(W . (a,b)) + (W . (b,c)) = W . (
a,
c) ) )
theorem Th33:
for
M being
MidSp for
W being
ATLAS of
M for
a,
b,
c,
d being
Point of
M for
x being
Vector of
W holds
(
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 being
Point of
M for
x being
Vector of
W ex
a being
Point of
M st
W . (
a,
b)
= x ) & (
W . (
b,
a)
= W . (
c,
a) implies
b = c ) & (
a @ b = c implies
W . (
a,
c)
= W . (
c,
b) ) & (
W . (
a,
c)
= W . (
c,
b) implies
a @ b = c ) & (
a @ b = c @ d implies
W . (
a,
d)
= W . (
c,
b) ) & (
W . (
a,
d)
= W . (
c,
b) implies
a @ b = c @ d ) & (
W . (
a,
b)
= x implies (
a,
x)
. W = b ) & ( (
a,
x)
. W = b implies
W . (
a,
b)
= x ) )