:: Atlas of Midpoint Algebra
:: by Micha{\l} Muzalewski
::
:: Received June 21, 1991
:: Copyright (c) 1991 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;
pred M,G are_associated_wrp w 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 are_associated_wrp 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
( M,G are_associated_wrp w 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 M,G are_associated_wrp w 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;
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 ) );

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 b₁ being Element of S st w . a,b₁ = x by A1, Def3;
uniqueness
for b₁, b₂ being Element of S st w . a,b₁ = x & w . a,b₂ = x holds
b₁ = b₂ 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 b₆ being Element of S holds
( b₆ = a,x . w iff w . a,b₆ = x );

theorem :: MIDSP_2:2

canceled;

theorem :: MIDSP_2:3

canceled;

theorem Th4: :: MIDSP_2:4

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

proof end;

theorem Th5: :: MIDSP_2:5

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

proof end;

theorem Th6: :: MIDSP_2:6

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)

proof end;

theorem Th7: :: MIDSP_2:7

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

proof end;

theorem Th8: :: MIDSP_2:8

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

proof end;

theorem Th9: :: MIDSP_2:9

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

proof end;

theorem Th10: :: MIDSP_2:10

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 & M,G are_associated_wrp w holds
p @ q = q @ p

proof end;

theorem Th11: :: MIDSP_2:11

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 & M,G are_associated_wrp w holds
ex r being Point of M st r @ p = q

proof end;

theorem :: MIDSP_2:12

canceled;

theorem Th13: :: MIDSP_2:13

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)

proof end;

theorem :: MIDSP_2:14

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

theorem Th15: :: MIDSP_2:15

for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x being Element of G holds Double (- x) = - (Double x)

proof end;

theorem Th16: :: MIDSP_2:16

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 & M,G are_associated_wrp w 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 Th17: :: MIDSP_2:17

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, b', c, c' being Element of S st w . a,b = w . b,c & w . a,b' = w . b',c' holds
w . c,c' = Double (w . b,b')

proof end;

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

end;

theorem Th18: :: MIDSP_2:18

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

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;

definition

let IT be non empty addLoopStr ;
attr IT 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 addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is midpoint_operator holds
b₁ is Fanoian

proof end;

end;

registration

cluster non empty strict right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
existence
ex b₁ being non empty addLoopStr st
( b₁ is strict & b₁ is midpoint_operator & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is Abelian )

proof end;

end;

theorem Th19: :: MIDSP_2:19

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

proof end;

theorem Th20: :: MIDSP_2:20

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

proof end;

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 b₁ being Element of G st Double b₁ = x by Def5;
uniqueness
for b₁, b₂ being Element of G st Double b₁ = x & Double b₂ = x holds
b₁ = b₂ by Th20;

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, b₃ being Element of G holds
( b₃ = Half x iff Double b₃ = x );

theorem :: MIDSP_2:21

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 )

proof end;

theorem Th22: :: MIDSP_2:22

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 & M,G are_associated_wrp w holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)

proof end;

theorem Th23: :: MIDSP_2:23

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 & M,G are_associated_wrp w holds
M is MidSp

proof end;

registration

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

proof end;

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

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 b₁ 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₁ . p,q = vect p,q

proof end;

uniqueness
for b₁, b₂ 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₁ . p,q = vect p,q ) & ( for p, q being Point of M holds b₂ . p,q = vect p,q ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines vect MIDSP_2:def 8 :

for M being MidSp
for b₂ being Function of [:the carrier of M,the carrier of M:],the carrier of (vectgroup M) holds
( b₂ = vect M iff for p, q being Point of M holds b₂ . p,q = vect p,q );

theorem Th24: :: MIDSP_2:24

for M being MidSp holds vect M is_atlas_of the carrier of M, vectgroup M

proof end;

theorem Th25: :: MIDSP_2:25

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 )

proof end;

theorem Th26: :: MIDSP_2:26

for M being MidSp
for p, q, r being Point of M holds
( p @ q = r iff vect p,r = vect r,q )

proof end;

theorem Th27: :: MIDSP_2:27

for M being MidSp holds M, vectgroup M are_associated_wrp vect M

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

proof end;

uniqueness
for b₁, b₂ being BinOp of S st ( for a, b being Element of S holds w . a,(b₁ . a,b) = w . (b₁ . a,b),b ) & ( for a, b being Element of S holds w . a,(b₂ . a,b) = w . (b₂ . a,b),b ) holds
b₁ = b₂

proof end;

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₄ being BinOp of S holds
( b₄ = @ w iff for a, b being Element of S holds w . a,(b₄ . a,b) = w . (b₄ . a,b),b );

theorem Th28: :: MIDSP_2:28

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 )

proof end;

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;

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 )

proof end;

theorem :: MIDSP_2:29

canceled;

theorem :: MIDSP_2:30

canceled;

theorem :: MIDSP_2:31

canceled;

theorem Th32: :: MIDSP_2:32

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
MidStr(# S,(@ w) #),G are_associated_wrp Atlas w

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

proof end;

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 Th33: :: MIDSP_2:33

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 & M,G are_associated_wrp w ) )

proof end;

definition

let M be non empty MidStr ;
attr c₂ is strict ;
struct AtlasStr of M -> ;
aggr AtlasStr(# algebra, function #) -> AtlasStr of M;
sel algebra c₂ -> non empty addLoopStr ;
sel function c₂ -> Function of [:the carrier of M,the carrier of M:],the carrier of the algebra of c₂;

end;

definition

let M be non empty MidStr ;
let IT be AtlasStr of 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 & 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;

:: deftheorem Def12 defines ATLAS-like MIDSP_2:def 12 :

for M being non empty MidStr
for IT being AtlasStr of 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 & 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 ) );

registration

let M be MidSp;
cluster ATLAS-like AtlasStr of M;
existence
ex b₁ being AtlasStr of M st b₁ is ATLAS-like

proof end;

end;

definition

let M be non empty MidSp;
mode ATLAS of M is ATLAS-like AtlasStr of M;

end;

definition

let M be non empty MidStr ;
let W be AtlasStr of M;
mode Vector of W is Element of the algebra of W;

end;

definition

let M be MidSp;
let W be AtlasStr of M;
let a, b be Point of M;
func W . 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 of 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 of 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 of 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 Th34: :: MIDSP_2:34

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

proof end;

theorem Th35: :: MIDSP_2:35

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 & M,G are_associated_wrp w holds
( a @ c = b iff w . a,c = Double (w . a,b) )

proof end;

theorem :: MIDSP_2:36

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

proof end;

theorem :: MIDSP_2:37

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

proof end;

theorem :: MIDSP_2:38

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

proof end;

theorem Th39: :: MIDSP_2:39

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

proof end;

theorem :: MIDSP_2:40

for M being MidSp
for W being ATLAS of M
for a being Point of M holds a,(0. W) . W = a

proof end;