:: by Micha{\l} Muzalewski

::

:: Received June 21, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

definition
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;

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;

end;
let G be non empty addLoopStr ;

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G;

attr w 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) );

for p, q, r being Point of M holds

( p @ q = r iff w . (p,r) = w . (r,q) );

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

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

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

proof end;

definition

let S be non empty set ;

let G be non empty addLoopStr ;

let w be Function of [:S,S:], the carrier of G;

end;
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: :: 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) ) );

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

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

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 ;

existence

ex b_{1} being Element of S st w . (a,b_{1}) = x
by A1, Def3;

uniqueness

for b_{1}, b_{2} being Element of S st w . (a,b_{1}) = x & w . (a,b_{2}) = x holds

b_{1} = b_{2}
by A1, Def3;

end;
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 ;

existence

ex b

uniqueness

for b

b

:: 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 b_{6} being Element of S holds

( b_{6} = (a,x) . w iff w . (a,b_{6}) = x );

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 b

( b

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

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

proof end;

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

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

proof end;

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

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

proof end;

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)

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)

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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)

for x, y, z, t being Element of G holds (x + y) + (z + t) = (x + z) + (y + t)

proof end;

theorem :: MIDSP_2:11

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)

for x being Element of G holds Double (- x) = - (Double x)

proof end;

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

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

proof end;

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

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

proof end;

registration

let M be MidSp;

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;
coherence

( vectgroup M is Abelian & vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable ) by MIDSP_1:56;

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

( ( 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 ) )

proof end;

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

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

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

coherence

for b_{1} being non empty addLoopStr st b_{1} is midpoint_operator holds

b_{1} is Fanoian

end;
for b

b

proof end;

registration

ex b_{1} being non empty addLoopStr st

( b_{1} is strict & b_{1} is midpoint_operator & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian )
end;

cluster non empty strict right_complementable Abelian add-associative right_zeroed midpoint_operator for addLoopStr ;

existence ex b

( b

proof 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

for x being Element of G st x = - x holds

x = 0. G

proof end;

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

for x, y being Element of G st Double x = Double y holds

x = y

proof end;

definition

let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;

let x be Element of G;

existence

ex b_{1} being Element of G st Double b_{1} = x
by Def5;

uniqueness

for b_{1}, b_{2} being Element of G st Double b_{1} = x & Double b_{2} = x holds

b_{1} = b_{2}
by Th17;

end;
let x be Element of G;

existence

ex b

uniqueness

for b

b

:: 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, b_{3} being Element of G holds

( b_{3} = Half x iff Double b_{3} = x );

for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr

for x, b

( b

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 )

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 )

proof end;

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)

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)

proof end;

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

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

proof end;

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

for M being MidSp

for p, q being Point of M holds vector (p,q) = vect (p,q);

definition

let M be MidSp;

ex b_{1} 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 b_{1} . (p,q) = vect (p,q)

for b_{1}, b_{2} 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 b_{1} . (p,q) = vect (p,q) ) & ( for p, q being Point of M holds b_{2} . (p,q) = vect (p,q) ) holds

b_{1} = b_{2}

end;
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 for p, q being Point of M holds it . (p,q) = vect (p,q);

ex b

for p, q being Point of M holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines vect MIDSP_2:def 8 :

for M being MidSp

for b_{2} being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) holds

( b_{2} = vect M iff for p, q being Point of M holds b_{2} . (p,q) = vect (p,q) );

for M being MidSp

for b

( b

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 )

for p, q, r, s being Point of M holds

( vect (p,q) = vect (r,s) iff p @ s = q @ r )

proof end;

Lm2: for M being MidSp holds vect M is associating

proof end;

registration
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 ;

ex b_{1} being BinOp of S st

for a, b being Element of S holds w . (a,(b_{1} . (a,b))) = w . ((b_{1} . (a,b)),b)

for b_{1}, b_{2} being BinOp of S st ( for a, b being Element of S holds w . (a,(b_{1} . (a,b))) = w . ((b_{1} . (a,b)),b) ) & ( for a, b being Element of S holds w . (a,(b_{2} . (a,b))) = w . ((b_{2} . (a,b)),b) ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of S holds w . (a,(it . (a,b))) = w . ((it . (a,b)),b);

ex b

for a, b being Element of S holds w . (a,(b

proof end;

uniqueness for b

b

proof 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 b_{4} being BinOp of S holds

( b_{4} = @ w iff for a, b being Element of S holds w . (a,(b_{4} . (a,b))) = w . ((b_{4} . (a,b)),b) );

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

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

proof end;

registration
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;

w is Function of [: the carrier of MidStr(# S,(@ w) #), the carrier of MidStr(# S,(@ w) #):], the carrier of G ;

end;
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;

w is Function of [: the carrier of MidStr(# S,(@ w) #), the carrier of MidStr(# S,(@ w) #):], the carrier of G ;

:: 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;

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

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

proof 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 ;

coherence

MidStr(# S,(@ w) #) is strict MidSp

end;
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 ;

coherence

MidStr(# S,(@ w) #) is strict MidSp

proof 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) #);

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

( 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 ) )

proof end;

definition

let M be non empty MidStr ;

attr c_{2} is strict ;

struct AtlasStr over M -> ;

aggr AtlasStr(# algebra, function #) -> AtlasStr over M;

sel algebra c_{2} -> non empty addLoopStr ;

sel function c_{2} -> Function of [: the carrier of M, the carrier of M:], the carrier of the algebra of c_{2};

end;
attr c

struct AtlasStr over M -> ;

aggr AtlasStr(# algebra, function #) -> AtlasStr over M;

sel algebra c

sel function c

definition

let M be non empty MidStr ;

let IT be AtlasStr over M;

end;
let IT be AtlasStr over M;

attr IT 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 );

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

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

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
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;
let W be AtlasStr over M;

mode Vector of W is Element of the algebra of W;

definition

let M be MidSp;

let W be AtlasStr over M;

let a, b be Point of M;

coherence

the function of W . (a,b) is Element of the algebra of W ;

end;
let W be AtlasStr over M;

let a, b be Point of M;

coherence

the function of W . (a,b) is Element of the algebra of W ;

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

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;

coherence

(a,x) . the function of W is Point of M ;

end;
let W be AtlasStr over M;

let a be Point of M;

let x be Vector of W;

coherence

(a,x) . the function of W is Point of M ;

:: 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;

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;

:: 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;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;