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

definition

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

end;

registration

cluster non empty for MidStr ;

existence
not for b₁ being MidStr holds b₁ 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(# {0},op2 #);

correctness
coherence
MidStr(# {0},op2 #) is MidStr ;
;

end;

:: deftheorem defines Example MIDSP_1:def 2 :
Example = MidStr(# {0},op2 #);

registration

cluster Example -> non empty strict ;

coherence
( Example is strict & not Example is empty ) ;

end;

theorem :: MIDSP_1:1

the carrier of Example = {{}} ;

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 b₁ being non empty MidStr st
( b₁ is strict & b₁ is MidSp-like ) by Def3, Th4;

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 a, x, 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 :: MIDSP_1:def 4
a @ d = b @ c;

end;

:: deftheorem 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 :: MIDSP_1:10

for M being MidSp
for a, b being Element of M holds a,a @@ b,b ;

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 ;

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 by Th8;

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 :: MIDSP_1:14

for M being MidSp
for a, b being Element of M holds a,b @@ a,b ;

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 by Th8;

theorem Th17: :: MIDSP_1:17

for M being MidSp
for a, b, c, d, x, y 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, c, a9, b9, 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 :: 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 ;
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 ;

end;

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

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 ;

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 by Th17;

theorem :: MIDSP_1:22

for M being MidSp
for p, q, r 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 b₁ 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 b₁ = p ~

proof end;

end;

:: deftheorem Def7 defines Vector MIDSP_1:def 7 :
for M being MidSp
for b₂ being non empty Subset of [: the carrier of M, the carrier of M:] holds
( b₂ is Vector of M iff ex p being Element of [: the carrier of M, the carrier of M:] st b₂ = 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 b₁ 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 & b₁ = [(p `1),(q `2)] ~ )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = [(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 & b₂ = [(p `1),(q `2)] ~ ) holds
b₁ = b₂ by Th33;

end;

:: deftheorem Def9 defines + MIDSP_1:def 9 :
for M being MidSp
for u, v, b₄ being Vector of M holds
( b₄ = 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 & b₄ = [(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 b₁ being Vector of M st u + b₁ = ID M by Th45;
uniqueness
for b₁, b₂ being Vector of M st u + b₁ = ID M & u + b₂ = ID M holds
b₁ = b₂ by Th47;

end;

:: deftheorem defines - MIDSP_1:def 11 :
for M being MidSp
for u, b₃ being Vector of M holds
( b₃ = - u iff u + b₃ = 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 b₁ being Element of setvect M st
for u, v being Vector of M st u1 = u & v1 = v holds
b₁ = u + v

proof end;

uniqueness
for b₁, b₂ being Element of setvect M st ( for u, v being Vector of M st u1 = u & v1 = v holds
b₁ = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds
b₂ = u + v ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines + MIDSP_1:def 13 :
for M being MidSp
for u1, v1, b₄ being Element of setvect M holds
( b₄ = u1 + v1 iff for u, v being Vector of M st u1 = u & v1 = v holds
b₄ = 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 b₁ being BinOp of (setvect M) st
for u1, v1 being Element of setvect M holds b₁ . (u1,v1) = u1 + v1

proof end;

uniqueness
for b₁, b₂ being BinOp of (setvect M) st ( for u1, v1 being Element of setvect M holds b₁ . (u1,v1) = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds b₂ . (u1,v1) = u1 + v1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines addvect MIDSP_1:def 14 :
for M being MidSp
for b₂ being BinOp of (setvect M) holds
( b₂ = addvect M iff for u1, v1 being Element of setvect M holds b₂ . (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 b₁ being UnOp of (setvect M) st
for W being Element of setvect M holds W + (b₁ . W) = ID M

proof end;

uniqueness
for b₁, b₂ being UnOp of (setvect M) st ( for W being Element of setvect M holds W + (b₁ . W) = ID M ) & ( for W being Element of setvect M holds W + (b₂ . W) = ID M ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines complvect MIDSP_1:def 15 :
for M being MidSp
for b₂ being UnOp of (setvect M) holds
( b₂ = complvect M iff for W being Element of setvect M holds W + (b₂ . 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;