:: Atlas of Midpoint Algebra
:: by Micha{\l} Muzalewski
::
:: Received June 21, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let G be non empty addLoopStr ;
let x be Element of G;
func Double x ->  Element of G equals :: MIDSP_2:def 1
x + x;
coherence
 x + x is Element of G ;
end;

:: deftheorem  defines Double MIDSP_2:def_1_:_
 for G being non empty addLoopStr
for x being Element of G holds Double x = x + x;

definition
let M be non empty MidStr ;
let G be non empty addLoopStr ;
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G;
attrw is associating  means :Def2: :: MIDSP_2:def 2
 for p, q, r being Point of M holds
( p @ q = r iff w . (p,r) = w . (r,q) );
end;

:: deftheorem Def2 defines associating MIDSP_2:def_2_:_
 for M being non empty MidStr
for G being non empty addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G holds
( w is associating iff for p, q, r being Point of M holds
( p @ q = r iff w . (p,r) = w . (r,q) ) );

theorem Th1: :: MIDSP_2:1
for G being non empty addLoopStr
for M being non empty MidStr
for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
proofend;

definition
let S be non empty set ;
let G be non empty addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
predw is_atlas_of S,G means :Def3: :: MIDSP_2:def 3
( ( 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: :: MIDSP_2:def 4
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_:_
 for S being non empty set
for G being non empty addLoopStr
for w being Function of [:S,S:], the carrier of G
for a being Element of S
for x being Element of G st w is_atlas_of S,G holds
for b6 being Element of S holds
( b6 = (a,x) . w iff w . (a,b6) = x );

theorem Th2: :: MIDSP_2:2
for S being non empty set
for a 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 holds
w . (a,a) = 0. G
proofend;

theorem Th3: :: MIDSP_2:3
for S being non empty set
for a, b 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) = 0. G holds
a = b
proofend;

theorem Th4: :: MIDSP_2:4
for S being non empty set
for a, b 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 holds
w . (a,b) = - (w . (b,a))
proofend;

theorem Th5: :: MIDSP_2:5
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)
proofend;

theorem Th6: :: MIDSP_2:6
for S being non empty set
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 holds
for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x
proofend;

theorem Th7: :: MIDSP_2:7
for S being non empty set
for b, a, c 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 . (b,a) = w . (c,a) holds
b = c
proofend;

theorem Th8: :: MIDSP_2:8
for M being non empty MidStr
for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for 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 holds
p @ q = q @ p
proofend;

theorem Th9: :: MIDSP_2:9
for M being non empty MidStr
for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for 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 holds
ex r being Point of M st r @ p = q
proofend;

theorem Th10: :: MIDSP_2:10
for G being non empty Abelian add-associative addLoopStr
for x, y, z, t being Element of G holds (x + y) + (z + t) = (x + z) + (y + t)
proofend;

theorem :: MIDSP_2:11
for G being non empty Abelian add-associative addLoopStr
for x, y being Element of G holds Double (x + y) = (Double x) + (Double y) by Th10;

theorem Th12: :: MIDSP_2:12
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x being Element of G holds Double (- x) = - (Double x)
proofend;

theorem Th13: :: MIDSP_2:13
for M being non empty MidStr
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for 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 holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
proofend;

theorem Th14: :: MIDSP_2:14
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))
proofend;

registration
let M be MidSp;
cluster vectgroup M ->  right_complementable Abelian add-associative right_zeroed ;
coherence
 ( vectgroup M is Abelian & vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable ) by MIDSP_1:56;
end;

theorem Th15: :: MIDSP_2:15
for M being MidSp holds
( ( 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)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
proofend;

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) ) )
proofend;

definition
let IT be non empty addLoopStr ;
attrIT is midpoint_operator  means :Def5: :: 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 st Double a = 0. IT holds
a = 0. IT ) );
end;

:: deftheorem Def5 defines midpoint_operator MIDSP_2:def_5_:_
 for IT being non empty addLoopStr holds
( IT is midpoint_operator iff ( ( for a being Element of IT ex x being Element of IT st Double x = a ) & ( for a being Element of IT st Double a = 0. IT holds
a = 0. IT ) ) );

registration
cluster non empty midpoint_operator  ->  non empty Fanoian for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is midpoint_operator holds
b1 is Fanoian
proofend;
end;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed midpoint_operator for addLoopStr ;
existence
 ex b1 being non empty addLoopStr st
( b1 is strict & b1 is midpoint_operator & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian )
proofend;
end;

theorem Th16: :: MIDSP_2:16
for G being non empty right_complementable Fanoian add-associative right_zeroed addLoopStr
for x being Element of G st x = - x holds
x = 0. G
proofend;

theorem Th17: :: MIDSP_2:17
for G being non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr
for x, y being Element of G st Double x = Double y holds
x = y
proofend;

definition
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let x be Element of G;
func Half x ->  Element of G means :Def6: :: MIDSP_2:def 6
 Double it = x;
existence
 ex b1 being Element of G st Double b1 = x by Def5;
uniqueness
 for b1, b2 being Element of G st Double b1 = x & Double b2 = x holds
b1 = b2 by Th17;
end;

:: deftheorem Def6 defines Half MIDSP_2:def_6_:_
 for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for x, b3 being Element of G holds
( b3 = Half x iff Double b3 = x );

theorem :: MIDSP_2:18
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for x, y being Element of G holds
( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )
proofend;

theorem Th19: :: MIDSP_2:19
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 st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
proofend;

theorem Th20: :: MIDSP_2:20
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 st w is_atlas_of the carrier of M,G & w is associating holds
M is MidSp
proofend;

registration
let M be MidSp;
cluster vectgroup M ->  midpoint_operator ;
coherence
 vectgroup M is midpoint_operator
proofend;
end;

definition
let M be MidSp;
let p, q be Point of M;
func vector (p,q) ->  Element of (vectgroup M) equals :: MIDSP_2:def 7
 vect (p,q);
coherence
 vect (p,q) is Element of (vectgroup M) by Th15;
end;

:: deftheorem  defines vector MIDSP_2:def_7_:_
 for M being MidSp
for p, q being Point of M holds vector (p,q) = vect (p,q);

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: :: MIDSP_2:def 8
 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)
proofend;
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
proofend;
end;

:: deftheorem Def8 defines vect MIDSP_2:def_8_:_
 for M being MidSp
for b2 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) holds
( b2 = vect M iff for p, q being Point of M holds b2 . (p,q) = vect (p,q) );

theorem Th21: :: MIDSP_2:21
for M being MidSp holds vect M is_atlas_of the carrier of M, vectgroup M
proofend;

theorem Th22: :: MIDSP_2:22
for M being MidSp
for p, q, r, s being Point of M holds
( vect (p,q) = vect (r,s) iff p @ s = q @ r )
proofend;

theorem Th23: :: MIDSP_2:23
for M being MidSp
for p, q, r being Point of M holds
( p @ q = r iff vect (p,r) = vect (r,q) )
proofend;

theorem :: MIDSP_2:24
canceled;

Lm2:  for M being MidSp holds vect M is associating
proofend;

registration
let M be MidSp;
cluster vect M ->  associating ;
coherence
 vect M is associating by Lm2;
end;

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: :: MIDSP_2:def 9
 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)
proofend;
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
proofend;
end;

:: deftheorem Def9 defines @ MIDSP_2:def_9_:_
 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 b4 being BinOp of S holds
( b4 = @ w iff for a, b being Element of S holds w . (a,(b4 . (a,b))) = w . ((b4 . (a,b)),b) );

theorem Th25: :: MIDSP_2:25
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 Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
proofend;

registration
let D be non empty set ;
let M be BinOp of D;
cluster MidStr(# D,M #) ->  non empty ;
coherence
 not MidStr(# D,M #) is empty ;
end;

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 :: MIDSP_2:def 10
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_:_
 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 holds Atlas w = w;

theorem Th26: :: MIDSP_2:26
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
Atlas w is associating
proofend;

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 MidSp. w ->  strict MidSp equals :: MIDSP_2:def 11
 MidStr(# S,(@ w) #);
coherence
 MidStr(# S,(@ w) #) is strict MidSp
proofend;
end;

:: deftheorem  defines MidSp. MIDSP_2:def_11_:_
 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
MidSp. w = MidStr(# S,(@ w) #);

theorem Th27: :: MIDSP_2:27
for M being non empty MidStr holds
( M is MidSp iff ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr 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 ) )
proofend;

definition
let M be non empty MidStr ;
attrc2 is strict ;
struct AtlasStr over M -> ;
aggrAtlasStr(# algebra, function #) ->  AtlasStr over M;
sel algebra c2 ->  non empty addLoopStr ;
sel function c2 ->  Function of [: the carrier of M, the carrier of M:], the carrier of the algebra of c2;
end;

definition
let M be non empty MidStr ;
let IT be AtlasStr over M;
attrIT is ATLAS-like  means :Def12: :: MIDSP_2:def 12
( the algebra of IT is midpoint_operator & the algebra of IT is add-associative & the algebra of IT is right_zeroed & the algebra of IT is right_complementable & the algebra of IT is Abelian & the function of IT is associating & the function of IT is_atlas_of the carrier of M, the algebra of IT );
end;

:: deftheorem Def12 defines ATLAS-like MIDSP_2:def_12_:_
 for M being non empty MidStr
for IT being AtlasStr over M holds
( IT is ATLAS-like iff ( the algebra of IT is midpoint_operator & the algebra of IT is add-associative & the algebra of IT is right_zeroed & the algebra of IT is right_complementable & the algebra of IT is Abelian & the function of IT is associating & the function of IT is_atlas_of the carrier of M, the algebra of IT ) );

registration
let M be MidSp;
cluster ATLAS-like for AtlasStr over M;
existence
 ex b1 being AtlasStr over M st b1 is ATLAS-like
proofend;
end;

definition
let M be MidSp;
mode ATLAS of M is ATLAS-like AtlasStr over M;
end;

definition
let M be non empty MidStr ;
let 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;
funcW . (a,b) ->  Element of the algebra of W equals :: MIDSP_2:def 13
 the function of W . (a,b);
coherence
 the function of W . (a,b) is Element of the algebra of W ;
end;

:: deftheorem  defines . MIDSP_2:def_13_:_
 for M being MidSp
for W being AtlasStr over M
for a, b being Point of M holds W . (a,b) = the function of W . (a,b);

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;
coherence
 (a,x) . the function of W is Point of M ;
end;

:: deftheorem  defines . MIDSP_2:def_14_:_
 for M being MidSp
for W being AtlasStr over M
for a being Point of M
for x being Vector of W holds (a,x) . W = (a,x) . the function of W;

definition
let M be MidSp;
let W be ATLAS of M;
func 0. W ->  Vector of W equals :: MIDSP_2:def 15
 0. the algebra of W;
coherence
 0. the algebra of W is Vector of W ;
end;

:: deftheorem  defines 0. MIDSP_2:def_15_:_
 for M being MidSp
for W being ATLAS of M holds 0. W = 0. the algebra of W;

theorem Th28: :: MIDSP_2:28
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 & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
proofend;

theorem Th29: :: MIDSP_2:29
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, b being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
proofend;

theorem :: MIDSP_2:30
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)) )
proofend;

theorem :: MIDSP_2:31
for M being MidSp
for W being ATLAS of M
for a, c, b being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
proofend;

theorem :: MIDSP_2:32
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) ) )
proofend;

theorem Th33: :: MIDSP_2:33
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 ) )
proofend;

theorem :: MIDSP_2:34
for M being MidSp
for W being ATLAS of M
for a being Point of M holds (a,(0. W)) . W = a
proofend;