:: by Micha{\l} Muzalewski

::

:: Received November 26, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct MidStr -> 1-sorted ;

aggr MidStr(# carrier, MIDPOINT #) -> MidStr ;

sel MIDPOINT c_{1} -> BinOp of the carrier of c_{1};

end;
struct MidStr -> 1-sorted ;

aggr MidStr(# carrier, MIDPOINT #) -> MidStr ;

sel MIDPOINT c

registration
end;

definition

let MS be non empty MidStr ;

let a, b be Element of MS;

coherence

the MIDPOINT of MS . (a,b) is Element of MS ;

end;
let a, b be Element of MS;

coherence

the MIDPOINT of MS . (a,b) is Element of MS ;

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

for MS being non empty MidStr

for a, b being Element of MS holds a @ b = the MIDPOINT of MS . (a,b);

registration
end;

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 )

( 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

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

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

existence

ex b_{1} being non empty MidStr st

( b_{1} is strict & b_{1} is MidSp-like )
by Def3, Th4;

end;
ex b

( b

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

theorem :: MIDSP_1:9

:: left-cancellation-law

:: B. CONGRUENCE RELATION

:: B. CONGRUENCE RELATION

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

for M being MidSp

for a, b, c, d being Element of M holds

( a,b @@ c,d iff a @ d = b @ c );

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

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

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

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;
let p, q be Element of [: the carrier of M, the carrier of M:];

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 ;

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

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

theorem :: MIDSP_1:23

theorem :: MIDSP_1:24

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

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

{ 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;
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 } ;

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

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

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

coherence

not p ~ is empty by Th25;

end;
let p be Element of [: the carrier of M, the carrier of M:];

coherence

not p ~ is empty by Th25;

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 )

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 ~

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

for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds

p ## q

proof end;

theorem :: MIDSP_1:30

definition

let M be MidSp;

ex b_{1} 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_{1} = p ~

end;
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 p being Element of [: the carrier of M, the carrier of M:] st it = p ~ ;

ex b

proof end;

:: deftheorem Def7 defines Vector MIDSP_1:def 7 :

for M being MidSp

for b_{2} being non empty Subset of [: the carrier of M, the carrier of M:] holds

( b_{2} is Vector of M iff ex p being Element of [: the carrier of M, the carrier of M:] st b_{2} = p ~ );

for M being MidSp

for b

( b

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

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 )

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;

{ p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } is Vector of M

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

{ p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } is Vector of M

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

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

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;

ex b_{1} 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_{1} = [(p `1),(q `2)] ~ )

for b_{1}, b_{2} 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_{1} = [(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_{2} = [(p `1),(q `2)] ~ ) holds

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

end;
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 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)] ~ );

ex b

( u = p ~ & v = q ~ & p `2 = q `1 & b

proof end;

uniqueness for b

( u = p ~ & v = q ~ & p `2 = q `1 & b

( u = p ~ & v = q ~ & p `2 = q `1 & b

b

:: deftheorem Def9 defines + MIDSP_1:def 9 :

for M being MidSp

for u, v, b_{4} being Vector of M holds

( b_{4} = 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_{4} = [(p `1),(q `2)] ~ ) );

for M being MidSp

for u, v, b

( b

( u = p ~ & v = q ~ & p `2 = q `1 & b

:: 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] ~

for a being Element of M

for u being Vector of M ex b being Element of M st u = [a,b] ~

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

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)

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

theorem :: MIDSP_1:37

:: F. VECTOR GROUPS

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)

for a, b being Element of M holds (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)

proof end;

definition

let M be MidSp;

let u be Vector of M;

existence

ex b_{1} being Vector of M st u + b_{1} = ID M
by Th45;

uniqueness

for b_{1}, b_{2} being Vector of M st u + b_{1} = ID M & u + b_{2} = ID M holds

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

end;
let u be Vector of M;

existence

ex b

uniqueness

for b

b

:: deftheorem defines - MIDSP_1:def 11 :

for M being MidSp

for u, b_{3} being Vector of M holds

( b_{3} = - u iff u + b_{3} = ID M );

for M being MidSp

for u, b

( b

definition

let M be MidSp;

{ X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } is set ;

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

{ X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } is set ;

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

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

registration
end;

definition

let M be MidSp;

let u1, v1 be Element of setvect M;

ex b_{1} being Element of setvect M st

for u, v being Vector of M st u1 = u & v1 = v holds

b_{1} = u + v

for b_{1}, b_{2} being Element of setvect M st ( for u, v being Vector of M st u1 = u & v1 = v holds

b_{1} = u + v ) & ( for u, v being Vector of M st u1 = u & v1 = v holds

b_{2} = u + v ) holds

b_{1} = b_{2}

end;
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 for u, v being Vector of M st u1 = u & v1 = v holds

it = u + v;

ex b

for u, v being Vector of M st u1 = u & v1 = v holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines + MIDSP_1:def 13 :

for M being MidSp

for u1, v1, b_{4} being Element of setvect M holds

( b_{4} = u1 + v1 iff for u, v being Vector of M st u1 = u & v1 = v holds

b_{4} = u + v );

for M being MidSp

for u1, v1, b

( b

b

definition

let M be MidSp;

ex b_{1} being BinOp of (setvect M) st

for u1, v1 being Element of setvect M holds b_{1} . (u1,v1) = u1 + v1

for b_{1}, b_{2} being BinOp of (setvect M) st ( for u1, v1 being Element of setvect M holds b_{1} . (u1,v1) = u1 + v1 ) & ( for u1, v1 being Element of setvect M holds b_{2} . (u1,v1) = u1 + v1 ) holds

b_{1} = b_{2}

end;
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 for u1, v1 being Element of setvect M holds it . (u1,v1) = u1 + v1;

ex b

for u1, v1 being Element of setvect M holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines addvect MIDSP_1:def 14 :

for M being MidSp

for b_{2} being BinOp of (setvect M) holds

( b_{2} = addvect M iff for u1, v1 being Element of setvect M holds b_{2} . (u1,v1) = u1 + v1 );

for M being MidSp

for b

( b

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

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;

ex b_{1} being UnOp of (setvect M) st

for W being Element of setvect M holds W + (b_{1} . W) = ID M

for b_{1}, b_{2} being UnOp of (setvect M) st ( for W being Element of setvect M holds W + (b_{1} . W) = ID M ) & ( for W being Element of setvect M holds W + (b_{2} . W) = ID M ) holds

b_{1} = b_{2}

end;
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 for W being Element of setvect M holds W + (it . W) = ID M;

ex b

for W being Element of setvect M holds W + (b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines complvect MIDSP_1:def 15 :

for M being MidSp

for b_{2} being UnOp of (setvect M) holds

( b_{2} = complvect M iff for W being Element of setvect M holds W + (b_{2} . W) = ID M );

for M being MidSp

for b

( b

definition

let M be MidSp;

addLoopStr(# (setvect M),(addvect M),(zerovect M) #) is addLoopStr ;

end;
func vectgroup M -> addLoopStr equals :: MIDSP_1:def 17

addLoopStr(# (setvect M),(addvect M),(zerovect M) #);

coherence addLoopStr(# (setvect M),(addvect M),(zerovect M) #);

addLoopStr(# (setvect M),(addvect M),(zerovect M) #) is addLoopStr ;

:: deftheorem defines vectgroup MIDSP_1:def 17 :

for M being MidSp holds vectgroup M = addLoopStr(# (setvect M),(addvect M),(zerovect M) #);

for M being MidSp holds vectgroup M = addLoopStr(# (setvect M),(addvect 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 )

( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )

proof end;