:: Midpoint algebras
:: by Micha{\l} Muzalewski
::
:: Received November 26, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
attr c1 is strict ;
struct MidStr -> 1-sorted ;
aggr MidStr(# carrier, MIDPOINT #) -> MidStr ;
sel MIDPOINT c1 -> BinOp of the carrier of c1;
end;

registration
cluster non empty for MidStr ;
existence
not for b1 being MidStr holds b1 is empty
proof end;
end;

definition
let MS be non empty MidStr ;
let a, b be Element of MS;
func a @ b -> Element of MS equals :: MIDSP_1:def 1
 the MIDPOINT of MS . (a,b);
coherence
the MIDPOINT of MS . (a,b) is Element of MS ;
end;

:: deftheorem defines @ MIDSP_1:def 1 :
for MS being non empty MidStr
for a, b being Element of MS holds a @ b = the MIDPOINT of MS . (a,b);

definition
func Example -> MidStr equals :: MIDSP_1:def 2
 MidStr(# 1,op2 #);
correctness
coherence
MidStr(# 1,op2 #) is MidStr ;
;
end;

:: deftheorem defines Example MIDSP_1:def 2 :
Example = MidStr(# 1,op2 #);

registration
cluster Example -> non empty strict ;
coherence
( Example is strict & not Example is empty ) ;
end;

theorem :: MIDSP_1:1
the carrier of Example = 1 ;

theorem :: MIDSP_1:2
the MIDPOINT of Example = op2 ;

theorem :: MIDSP_1:3
for a, b being Element of Example holds a @ b = op2 . (a,b) ;

theorem Th4: :: MIDSP_1:4
for a, b, c, d being Element of Example holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )
proof end;

:: A. MIDPOINT ALGEBRAS
definition
let IT be non empty MidStr ;
attr IT is MidSp-like means :Def3: :: MIDSP_1:def 3
 for a, b, c, d being Element of IT holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of IT st x @ a = b );
end;

:: deftheorem Def3 defines MidSp-like MIDSP_1:def 3 :
for IT being non empty MidStr holds
( IT is MidSp-like iff for a, b, c, d being Element of IT holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of IT st x @ a = b ) );

registration
cluster non empty strict MidSp-like for MidStr ;
existence
ex b1 being non empty MidStr st
( b1 is strict & b1 is MidSp-like )
proof end;
end;

definition
mode MidSp is non empty MidSp-like MidStr ;
end;

definition
let M be MidSp;
let a, b be Element of M;
:: original: @
redefine func a @ b -> Element of M;
commutativity
for a, b being Element of M holds a @ b = b @ a by Def3;
end;

theorem Th5: :: MIDSP_1:5
for M being MidSp
for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)
proof end;

theorem Th6: :: MIDSP_1:6
for M being MidSp
for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)
proof end;

theorem Th7: :: MIDSP_1:7
for M being MidSp
for a, b being Element of M st a @ b = a holds
a = b
proof end;

theorem Th8: :: MIDSP_1:8
for M being MidSp
for x, a, x9 being Element of M st x @ a = x9 @ a holds
x = x9
proof end;

theorem :: MIDSP_1:9
for M being MidSp
for a, x, x9 being Element of M st a @ x = a @ x9 holds
x = x9 by Th8;

:: left-cancellation-law
:: B. CONGRUENCE RELATION
definition
let M be MidSp;
let a, b, c, d be Element of M;
pred a,b @@ c,d means :Def4: :: MIDSP_1:def 4
a @ d = b @ c;
end;

:: deftheorem Def4 defines @@ MIDSP_1:def 4 :
for M being MidSp
for a, b, c, d being Element of M holds
( a,b @@ c,d iff a @ d = b @ c );

theorem Th10: :: MIDSP_1:10
for M being MidSp
for a, b being Element of M holds a,a @@ b,b
proof end;

theorem Th11: :: MIDSP_1:11
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b
proof end;

theorem Th12: :: MIDSP_1:12
for M being MidSp
for a, b, c being Element of M st a,a @@ b,c holds
b = c
proof end;

theorem Th13: :: MIDSP_1:13
for M being MidSp
for a, b, c being Element of M st a,b @@ c,c holds
a = b by Th11, Th12;

theorem Th14: :: MIDSP_1:14
for M being MidSp
for a, b being Element of M holds a,b @@ a,b
proof end;

theorem Th15: :: MIDSP_1:15
for M being MidSp
for a, b, c being Element of M ex d being Element of M st a,b @@ c,d
proof end;

theorem Th16: :: MIDSP_1:16
for M being MidSp
for a, b, c, d, d9 being Element of M st a,b @@ c,d & a,b @@ c,d9 holds
d = d9
proof end;

theorem Th17: :: MIDSP_1:17
for M being MidSp
for x, y, a, b, c, d being Element of M st x,y @@ a,b & x,y @@ c,d holds
a,b @@ c,d
proof end;

theorem Th18: :: MIDSP_1:18
for M being MidSp
for a, b, a9, b9, c, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds
a,c @@ a9,c9
proof end;

definition
let M be MidSp;
let p, q be Element of [: the carrier of M, the carrier of M:];
pred p ## q means :Def5: :: MIDSP_1:def 5
p `1 ,p `2 @@ q `1 ,q `2 ;
reflexivity
for p being Element of [: the carrier of M, the carrier of M:] holds p `1 ,p `2 @@ p `1 ,p `2 by Th14;
symmetry
for p, q being Element of [: the carrier of M, the carrier of M:] st p `1 ,p `2 @@ q `1 ,q `2 holds
q `1 ,q `2 @@ p `1 ,p `2 by Th11;
end;

:: deftheorem Def5 defines ## MIDSP_1:def 5 :
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] holds
( p ## q iff p `1 ,p `2 @@ q `1 ,q `2 );

theorem Th19: :: MIDSP_1:19
for M being MidSp
for a, b, c, d being Element of M st a,b @@ c,d holds
[a,b] ## [c,d]
proof end;

theorem Th20: :: MIDSP_1:20
for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
a,b @@ c,d
proof end;

theorem Th21: :: MIDSP_1:21
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & p ## r holds
q ## r
proof end;

theorem :: MIDSP_1:22
for M being MidSp
for p, r, q being Element of [: the carrier of M, the carrier of M:] st p ## r & q ## r holds
p ## q by Th21;

theorem :: MIDSP_1:23
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & q ## r holds
p ## r by Th21;

theorem :: MIDSP_1:24
for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q holds
( r ## p iff r ## q ) by Th21;

theorem Th25: :: MIDSP_1:25
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } is non empty Subset of [: the carrier of M, the carrier of M:]
proof end;

:: D. ( FREE ) VECTORS
definition
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
func p ~ -> Subset of [: the carrier of M, the carrier of M:] equals :: MIDSP_1:def 6
 { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } ;
coherence
{ q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } is Subset of [: the carrier of M, the carrier of M:] by Th25;
end;

:: deftheorem defines ~ MIDSP_1:def 6 :
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds p ~ = { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } ;

registration
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
cluster p ~ -> non empty ;
coherence
not p ~ is empty by Th25;
end;

theorem Th26: :: MIDSP_1:26
for M being MidSp
for r, p being Element of [: the carrier of M, the carrier of M:] holds
( r in p ~ iff r ## p )
proof end;

theorem Th27: :: MIDSP_1:27
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] st p ## q holds
p ~ = q ~
proof end;

theorem Th28: :: MIDSP_1:28
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds
p ## q
proof end;

theorem Th29: :: MIDSP_1:29
for M being MidSp
for a, b, c, d being Element of M st [a,b] ~ = [c,d] ~ holds
a @ d = b @ c
proof end;

theorem :: MIDSP_1:30
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds p in p ~ ;

definition
let M be MidSp;
mode Vector of M -> non empty Subset of [: the carrier of M, the carrier of M:] means :Def7: :: MIDSP_1:def 7
 ex p being Element of [: the carrier of M, the carrier of M:] st it = p ~ ;
existence
ex b1 being non empty Subset of [: the carrier of M, the carrier of M:] ex p being Element of [: the carrier of M, the carrier of M:] st b1 = p ~
proof end;
end;

:: deftheorem Def7 defines Vector MIDSP_1:def 7 :
for M being MidSp
for b2 being non empty Subset of [: the carrier of M, the carrier of M:] holds
( b2 is Vector of M iff ex p being Element of [: the carrier of M, the carrier of M:] st b2 = p ~ );

definition
let M be MidSp;
let p be Element of [: the carrier of M, the carrier of M:];
:: original: ~
redefine func p ~ -> Vector of M;
coherence
p ~ is Vector of M by Def7;
end;

theorem Th31: :: MIDSP_1:31
for M being MidSp ex u being Vector of M st
for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 )
proof end;

definition
let M be MidSp;
func ID M -> Vector of M equals :: MIDSP_1:def 8
 { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ;
coherence
{ p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } is Vector of M
proof end;
end;

:: deftheorem defines ID MIDSP_1:def 8 :
for M being MidSp holds ID M = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ;

theorem Th32: :: MIDSP_1:32
for M being MidSp
for b being Element of M holds ID M = [b,b] ~
proof end;

theorem Th33: :: MIDSP_1:33
for M being MidSp
for u, v, w, w9 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & w9 = [(p `1),(q `2)] ~ ) holds
w = w9
proof end;

definition
let M be MidSp;
let u, v be Vector of M;
func u + v -> Vector of M means :Def9: :: MIDSP_1:def 9
 ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & it = [(p `1),(q `2)] ~ );
existence
ex b1 being Vector of M ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ )
proof end;
uniqueness
for b1, b2 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b2 = [(p `1),(q `2)] ~ ) holds
b1 = b2 by Th33;
end;

:: deftheorem Def9 defines + MIDSP_1:def 9 :
for M being MidSp
for u, v, b4 being Vector of M holds
( b4 = u + v iff ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b4 = [(p `1),(q `2)] ~ ) );

:: E. ATLAS
theorem Th34: :: MIDSP_1:34
for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = [a,b] ~
proof end;

definition
let M be MidSp;
let a, b be Element of M;
func vect (a,b) -> Vector of M equals :: MIDSP_1:def 10
[a,b] ~ ;
coherence
[a,b] ~ is Vector of M ;
end;

:: deftheorem defines vect MIDSP_1:def 10 :
for M being MidSp
for a, b being Element of M holds vect (a,b) = [a,b] ~ ;

theorem Th35: :: MIDSP_1:35
for M being MidSp
for a being Element of M
for u being Vector of M ex b being Element of M st u = vect (a,b)
proof end;

theorem :: MIDSP_1:36
for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
vect (a,b) = vect (c,d) by Th27;

theorem :: MIDSP_1:37
for M being MidSp
for a, b, c, d being Element of M st vect (a,b) = vect (c,d) holds
a @ d = b @ c by Th29;

theorem :: MIDSP_1:38
for M being MidSp
for b being Element of M holds ID M = vect (b,b) by Th32;

theorem :: MIDSP_1:39
for M being MidSp
for a, b, c being Element of M st vect (a,b) = vect (a,c) holds
b = c
proof end;

theorem Th40: :: MIDSP_1:40
for M being MidSp
for a, b, c being Element of M holds (vect (a,b)) + (vect (b,c)) = vect (a,c)
proof end;

:: F. VECTOR GROUPS
theorem Th41: :: MIDSP_1:41
for M being MidSp
for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]
proof end;

theorem :: MIDSP_1:42
for M being MidSp
for a, b being Element of M holds (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)
proof end;

theorem Th43: :: MIDSP_1:43
for M being MidSp
for u, v, w being Vector of M holds (u + v) + w = u + (v + w)
proof end;

theorem Th44: :: MIDSP_1:44
for M being MidSp
for u being Vector of M holds u + (ID M) = u
proof end;

theorem Th45: :: MIDSP_1:45
for M being MidSp
for u being Vector of M ex v being Vector of M st u + v = ID M
proof end;

theorem Th46: :: MIDSP_1:46
for M being MidSp
for u, v being Vector of M holds u + v = v + u
proof end;

theorem Th47: :: MIDSP_1:47
for M being MidSp
for u, v, w being Vector of M st u + v = u + w holds
v = w
proof end;

definition
let M be MidSp;
let u be Vector of M;
func - u -> Vector of M means :: MIDSP_1:def 11
u + it = ID M;
existence
ex b1 being Vector of M st u + b1 = ID M by Th45;
uniqueness
for b1, b2 being Vector of M st u + b1 = ID M & u + b2 = ID M holds
b1 = b2 by Th47;
end;

:: deftheorem defines - MIDSP_1:def 11 :
for M being MidSp
for u, b3 being Vector of M holds
( b3 = - u iff u + b3 = ID M );

definition
let M be MidSp;
func setvect M -> set equals :: MIDSP_1:def 12
 { X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } ;
coherence
{ X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } is set ;
end;

:: deftheorem defines setvect MIDSP_1:def 12 :
for M being MidSp holds setvect M = { X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } ;

theorem Th48: :: MIDSP_1:48
for M being MidSp
for x being set holds
( x is Vector of M iff x in setvect M )
proof end;

registration
let M be MidSp;
cluster setvect M -> non empty ;
coherence
not setvect M is empty
proof end;
end;

definition
let M be MidSp;
let u1, v1 be Element of setvect M;
func u1 + v1 -> Element of setvect M means :Def13: :: MIDSP_1:def 13
 for u, v being Vector of M st u1 = u & v1 = v holds
it = u + v;
existence
ex b1 being Element of setvect M st
for u, v being Vector of M st u1 = u & v1 = v holds
b1 = u + v
proof end;
uniqueness
for b1, b2 being Element of setvect M st ( for u, v being Vector of M st u1 = u & v1 = v holds
b1 = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds
b2 = u + v ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines + MIDSP_1:def 13 :
for M being MidSp
for u1, v1, b4 being Element of setvect M holds
( b4 = u1 + v1 iff for u, v being Vector of M st u1 = u & v1 = v holds
b4 = u + v );

theorem Th49: :: MIDSP_1:49
for M being MidSp
for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1
proof end;

theorem Th50: :: MIDSP_1:50
for M being MidSp
for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)
proof end;

definition
let M be MidSp;
func addvect M -> BinOp of (setvect M) means :Def14: :: MIDSP_1:def 14
 for u1, v1 being Element of setvect M holds it . (u1,v1) = u1 + v1;
existence
ex b1 being BinOp of (setvect M) st
for u1, v1 being Element of setvect M holds b1 . (u1,v1) = u1 + v1
proof end;
uniqueness
for b1, b2 being BinOp of (setvect M) st ( for u1, v1 being Element of setvect M holds b1 . (u1,v1) = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds b2 . (u1,v1) = u1 + v1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines addvect MIDSP_1:def 14 :
for M being MidSp
for b2 being BinOp of (setvect M) holds
( b2 = addvect M iff for u1, v1 being Element of setvect M holds b2 . (u1,v1) = u1 + v1 );

theorem Th51: :: MIDSP_1:51
for M being MidSp
for W being Element of setvect M ex T being Element of setvect M st W + T = ID M
proof end;

theorem Th52: :: MIDSP_1:52
for M being MidSp
for W, W1, W2 being Element of setvect M st W + W1 = ID M & W + W2 = ID M holds
W1 = W2
proof end;

definition
let M be MidSp;
func complvect M -> UnOp of (setvect M) means :Def15: :: MIDSP_1:def 15
 for W being Element of setvect M holds W + (it . W) = ID M;
existence
ex b1 being UnOp of (setvect M) st
for W being Element of setvect M holds W + (b1 . W) = ID M
proof end;
uniqueness
for b1, b2 being UnOp of (setvect M) st ( for W being Element of setvect M holds W + (b1 . W) = ID M ) & ( for W being Element of setvect M holds W + (b2 . W) = ID M ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines complvect MIDSP_1:def 15 :
for M being MidSp
for b2 being UnOp of (setvect M) holds
( b2 = complvect M iff for W being Element of setvect M holds W + (b2 . W) = ID M );

definition
let M be MidSp;
func zerovect M -> Element of setvect M equals :: MIDSP_1:def 16
 ID M;
coherence
ID M is Element of setvect M by Th48;
end;

:: deftheorem defines zerovect MIDSP_1:def 16 :
for M being MidSp holds zerovect M = ID M;

definition
let M be MidSp;
func vectgroup M -> addLoopStr equals :: MIDSP_1:def 17
 addLoopStr(# (setvect M),(addvect M),(zerovect M) #);
coherence
addLoopStr(# (setvect M),(addvect M),(zerovect M) #) is addLoopStr ;
end;

:: deftheorem defines vectgroup MIDSP_1:def 17 :
for M being MidSp holds vectgroup M = addLoopStr(# (setvect M),(addvect M),(zerovect M) #);

registration
let M be MidSp;
cluster vectgroup M -> non empty strict ;
coherence
( vectgroup M is strict & not vectgroup M is empty ) ;
end;

theorem :: MIDSP_1:53
for M being MidSp holds the carrier of (vectgroup M) = setvect M ;

theorem :: MIDSP_1:54
for M being MidSp holds the addF of (vectgroup M) = addvect M ;

theorem :: MIDSP_1:55
for M being MidSp holds 0. (vectgroup M) = zerovect M ;

theorem :: MIDSP_1:56
for M being MidSp holds
( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
proof end;