begin
:: deftheorem defines Double MIDSP_2:def 1 :
:: deftheorem Def2 defines are_associated_wrp MIDSP_2:def 2 :
theorem Th1:
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 ) ) );
definition
let S be non
empty set ;
let G be non
empty addLoopStr ;
let w be
Function of
[:S,S:],the
carrier of
G;
let a be
Element of
S;
let x be
Element of
G;
assume A1:
w is_atlas_of S,
G
;
func a,
x . w -> Element of
S means :
Def4:
w . a,
it = x;
existence
ex b1 being Element of S st w . a,b1 = x
by A1, Def3;
uniqueness
for b1, b2 being Element of S st w . a,b1 = x & w . a,b2 = x holds
b1 = b2
by A1, Def3;
end;
:: deftheorem Def4 defines . MIDSP_2:def 4 :
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
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 Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
canceled;
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
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)
theorem Th18:
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) ) )
:: deftheorem Def5 defines midpoint_operator MIDSP_2:def 5 :
theorem Th19:
theorem Th20:
:: deftheorem Def6 defines Half MIDSP_2:def 6 :
theorem
theorem Th22:
theorem Th23:
:: deftheorem defines vector MIDSP_2:def 7 :
definition
let M be
MidSp;
func vect M -> Function of
[:the carrier of M,the carrier of M:],the
carrier of
(vectgroup M) means :
Def8:
for
p,
q being
Point of
M holds
it . p,
q = vect p,
q;
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;
:: deftheorem Def8 defines vect MIDSP_2:def 8 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
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;
:: deftheorem Def9 defines @ MIDSP_2:def 9 :
theorem Th28:
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;
func Atlas w -> Function of
[:the carrier of MidStr(# S,(@ w) #),the carrier of MidStr(# S,(@ w) #):],the
carrier of
G equals
w;
coherence
w is Function of [:the carrier of MidStr(# S,(@ w) #),the carrier of MidStr(# S,(@ w) #):],the carrier of G
;
end;
:: deftheorem defines Atlas MIDSP_2:def 10 :
Lm2:
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:],the carrier of G st w is_atlas_of S,G holds
for a, b, c being Point of MidStr(# S,(@ w) #) holds
( a @ b = c iff (Atlas w) . a,c = (Atlas w) . c,b )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th32:
:: deftheorem defines MidSp. MIDSP_2:def 11 :
theorem Th33:
:: deftheorem Def12 defines ATLAS-like MIDSP_2:def 12 :
:: deftheorem defines . MIDSP_2:def 13 :
:: deftheorem defines . MIDSP_2:def 14 :
:: deftheorem defines 0. MIDSP_2:def 15 :
theorem Th34:
for
G being non
empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr for
M being non
empty MidStr for
w being
Function of
[:the carrier of M,the carrier of M:],the
carrier of
G for
a,
c,
b1,
b2 being
Point of
M st
w is_atlas_of the
carrier of
M,
G &
M,
G are_associated_wrp w holds
(
a @ c = b1 @ b2 iff
w . a,
c = (w . a,b1) + (w . a,b2) )
theorem Th35:
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
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 Th39:
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 ) )
theorem