:: Midpoint algebras
:: by Micha{\l} Muzalewski
::
:: Received November 26, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, QC_LANG1, FUNCT_1,
FUNCT_5, ZFMISC_1, MCART_1, RELAT_1, VECTSP_1, ARYTM_3, ARYTM_1,
ALGSTR_0, SUPINF_2, RLVECT_1, MIDSP_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, MCART_1, DOMAIN_1,
ORDINAL1, FUNCT_2, FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1;
constructors BINOP_1, DOMAIN_1, RLVECT_1, FUNCT_5, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions STRUCT_0, RLVECT_1, ALGSTR_0;
equalities STRUCT_0, ALGSTR_0, ORDINAL1;
theorems FUNCT_2, TARSKI, BINOP_1;
schemes FUNCT_2, BINOP_1;
begin :: PRELIMINARY
definition
struct(1-sorted) MidStr (# carrier -> set, MIDPOINT -> BinOp of the carrier
#);
end;
registration
cluster non empty for MidStr;
existence
proof
set A = the non empty set,m = the BinOp of A;
take MidStr(#A,m#);
thus the carrier of MidStr(#A,m#) is non empty;
end;
end;
reserve MS for non empty MidStr;
reserve a, b for Element of MS;
definition
let MS,a,b;
func a@b -> Element of MS equals
(the MIDPOINT of MS).(a,b);
coherence;
end;
definition
func Example -> MidStr equals
MidStr (# {0}, op2 #);
correctness;
end;
registration
cluster Example -> strict non empty;
coherence;
end;
theorem
the carrier of Example = {{}};
theorem
the MIDPOINT of Example = op2;
theorem
for a,b being Element of Example holds a@b = op2.(a,b);
theorem Th4:
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
let a,b,c,d be Element of Example;
thus a@a = {} by TARSKI:def 1
.= a by TARSKI:def 1;
thus a@b = {} by TARSKI:def 1
.= b@a by TARSKI:def 1;
thus (a@b)@(c@d) = {} by TARSKI:def 1
.= (a@c)@(b@d) by TARSKI:def 1;
take x = a;
thus x@a = {} by TARSKI:def 1
.= b by TARSKI:def 1;
end;
:: A. MIDPOINT ALGEBRAS
definition
let IT be non empty MidStr;
attr IT is MidSp-like means
:Def3:
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;
registration
cluster strict MidSp-like for non empty MidStr;
existence
by Def3,Th4;
end;
definition
mode MidSp is MidSp-like non empty MidStr;
end;
definition
let M be MidSp, a, b be Element of M;
redefine func a@b; :: redefines @ (MIDSP_1, definition)
commutativity by Def3;
end;
reserve M for MidSp;
reserve a,b,c,d,a9,b9,c9,d9,x,y,x9 for Element of M;
theorem Th5:
(a@b)@c = (a@c)@(b@c)
proof
(a@b)@c = (a@b)@(c@c) by Def3
.= (a@c)@(b@c) by Def3;
hence thesis;
end;
theorem Th6: :: right-self-distributivity
a@(b@c) = (a@b)@(a@c)
proof
a@(b@c) = (a@a)@(b@c) by Def3
.= (a@b)@(a@c) by Def3;
hence thesis;
end;
theorem Th7: :: left-self-distributivity
a@b = a implies a = b
proof
assume
A1: a@b = a;
consider x such that
A2: x@a = b by Def3;
b = (x@a)@b by A2,Def3
.= (x@b)@a by A1,Th5
.= a by A1,A2,Th5;
hence thesis;
end;
theorem Th8:
x@a = x9@a implies x = x9
proof
assume
A1: x@a = x9@a;
consider y such that
A2: y@a = x by Def3;
x = x@(y@a) by A2,Def3
.= (x@y)@(x9@a) by A1,Th6
.= x@(x@x9) by A2,Def3;
then x = x@x9 by Th7;
hence thesis by Th7;
end;
theorem :: right-cancellation-law
a@x = a@x9 implies x = x9 by Th8;
:: left-cancellation-law
:: B. CONGRUENCE RELATION
definition
let M,a,b,c,d;
pred a,b @@ c,d means :: bound-vectors ab, cd are equivalent
a@d = b@c;
end;
theorem
a,a @@ b,b;
theorem Th11:
a,b @@ c,d implies c,d @@ a,b;
theorem Th12:
a,a @@ b,c implies b = c
by Th8;
theorem Th13:
a,b @@ c,c implies a = b by Th11,Th12;
theorem
a,b @@ a,b;
theorem Th15:
ex d st a,b @@ c,d
proof
consider d such that
A1: d@a =b@c by Def3;
a,b @@ c,d by A1;
hence thesis;
end;
theorem Th16:
a,b @@ c,d & a,b @@ c,d9 implies d = d9
by Th8;
theorem Th17:
x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d
proof
assume
A1: x,y @@ a,b;
assume
A2: x,y @@ c,d;
(y@x)@(a@d) = (y@a)@(x@d) by Def3
.= (x@b)@(x@d) by A1
.= (x@b)@(y@c) by A2
.= (y@x)@(b@c) by Def3;
hence a@d = b@c by Th8;
end;
theorem Th18:
a,b @@ a9,b9 & b,c @@ b9,c9 implies a,c @@ a9,c9
proof
assume
A1: a,b @@ a9,b9;
assume
A2: b,c @@ b9,c9;
(b9@b)@(a@c9) = (a@b9)@(b@c9) by Def3
.= (b@a9)@(b@c9) by A1
.= (c@b9)@(b@a9) by A2
.= (b9@b)@(c@a9) by Def3;
hence a@c9 = c@a9 by Th8;
end;
:: C. BOUND-VECTORS
reserve p,q,r,p9,q9 for Element of [:the carrier of M,the carrier of M:];
definition
let M,p,q;
pred p ## q means
p`1,p`2 @@ q`1,q`2;
reflexivity;
symmetry;
end;
theorem Th19:
a,b @@ c,d implies [a,b] ## [c,d];
theorem Th20:
[a,b] ## [c,d] implies a,b @@ c,d;
theorem Th21:
p ## q & p ## r implies q ## r by Th17;
theorem
p ## r & q ## r implies p ## q by Th21;
theorem
p ## q & q ## r implies p ## r by Th21;
theorem
p ## q implies (r ## p iff r ## q) by Th21;
theorem Th25:
for p holds { q : q ## p } is non empty Subset of [:the carrier
of M,the carrier of M:]
proof
let p;
set pp = { q : q ## p };
A1: for x be object holds x in pp implies x in [:the carrier of M,the carrier
of M:]
proof
let x be object;
assume x in pp;
then ex q st x = q & q ## p;
hence thesis;
end;
p in pp;
hence thesis by A1,TARSKI:def 3;
end;
:: D. ( FREE ) VECTORS
definition
let M,p;
func p~ -> Subset of [:the carrier of M,the carrier of M:] equals
{ q : q ## p};
coherence by Th25;
end;
registration
let M,p;
cluster p~ -> non empty;
coherence by Th25;
end;
theorem Th26:
for p holds r in p~ iff r ## p
proof
let p;
thus r in p~ implies r ## p
proof
assume r in p~;
then ex q st r = q & q ## p;
hence thesis;
end;
thus thesis;
end;
theorem Th27:
p ## q implies p~ = q~
proof
assume
A1: p ## q;
for x being object holds x in p~ iff x in q~
proof
let x be object;
thus x in p~ implies x in q~
proof
assume
A2: x in p~;
then reconsider
r = x as Element of [:the carrier of M,the carrier of M:];
r ## p by A2,Th26;
then r ## q by A1,Th21;
hence thesis;
end;
thus x in q~ implies x in p~
proof
assume
A3: x in q~;
then reconsider
r = x as Element of [:the carrier of M,the carrier of M:];
r ## q by A3,Th26;
then r ## p by A1,Th21;
hence thesis;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th28:
p~ = q~ implies p ## q
proof
p in p~;
hence thesis by Th26;
end;
theorem Th29:
[a,b]~ = [c,d]~ implies a@d = b@c
proof
assume [a,b]~ = [c,d]~;
then a,b @@ c,d by Th20,Th28;
hence thesis;
end;
theorem
p in p~;
definition
let M;
mode Vector of M -> non empty Subset of [:the carrier of M,the carrier of M
:] means
:Def7:
ex p st it = p~;
existence
proof
set p = the Element of [:the carrier of M,the carrier of M:];
take p~;
thus thesis;
end;
end;
reserve u,v,w,u9,w9 for Vector of M;
definition
let M,p;
redefine func p~ -> Vector of M; :: redefines ~ (MIDSP_1, definition)
coherence by Def7;
end;
theorem Th31:
ex u st for p holds p in u iff p`1 = p`2
proof
set a = the Element of M;
take [a,a]~;
let p;
p`1,p`2 @@ a,a iff p ## [a,a];
hence thesis by Th13,Th26;
end;
definition
let M;
func ID(M) -> Vector of M equals :: zero vector
{ p : p`1 = p`2 };
coherence
proof
consider u such that
A1: for p holds p in u iff p`1 = p`2 by Th31;
u = { p : p`1 = p`2 }
proof
for x being object holds x in u iff x in { p : p`1 = p`2 }
proof
let x be object;
thus x in u implies x in { p : p`1 = p`2 }
proof
assume
A2: x in u;
then reconsider
r = x as Element of [:the carrier of M,the carrier of M:];
r`1 = r`2 by A1,A2;
hence thesis;
end;
thus x in { p : p`1 = p`2 } implies x in u
proof
assume x in { p : p`1 = p`2 };
then ex p st x = p & p`1 = p`2;
hence thesis by A1;
end;
end;
hence thesis by TARSKI:2;
end;
hence thesis;
end;
end;
theorem Th32:
ID(M) = [b,b]~
proof
p in ID(M) iff p in [b,b]~
proof
thus p in ID(M) implies p in [b,b]~
proof
assume p in ID(M);
then ex q st p = q & q`1 = q`2;
then
A1: p`1,p`2 @@ b,b;
p ## [b,b] by A1;
hence thesis;
end;
thus p in [b,b]~ implies p in ID(M)
proof
assume p in [b,b]~;
then
A2: p ## [b,b] by Th26;
p`1,p`2 @@ b,b by A2;
then p`1 = p`2 by Th11,Th12;
hence thesis;
end;
end;
then for p being object holds p in ID(M) iff p in [b,b]~;
hence thesis by TARSKI:2;
end;
theorem Th33:
(ex p,q st u = p~ & v = q~ & p`2 = q`1 & w = [p`1,q`2]~)& (ex p,
q st u = p~ & v = q~ & p`2 = q`1 & w9 = [p`1,q`2]~) implies w = w9
proof
given p,q such that
A1: u = p~ and
A2: v = q~ and
A3: p`2 = q`1 and
A4: w = [p`1,q`2]~;
given p9,q9 such that
A5: u = p9~ and
A6: v = q9~ and
A7: p9`2 = q9`1 and
A8: w9 = [p9`1,q9`2]~;
q ## q9 by A2,A6,Th28;
then
A9: q`1,q`2 @@ q9`1,q9`2;
p ## p9 by A1,A5,Th28;
then p`1,p`2 @@ p9`1,p9`2;
then p`1,q`2 @@ p9`1,q9`2 by A3,A7,A9,Th18;
hence thesis by A4,A8,Th19,Th27;
end;
definition
let M,u,v;
func u + v -> Vector of M means
:Def9:
ex p,q st u = p~ & v = q~ & p`2 = q `1 & it = [p`1,q`2]~;
existence
proof
consider p such that
A1: u = p~ by Def7;
consider q such that
A2: v = q~ by Def7;
consider d such that
A3: q`1,q`2 @@ p`2,d by Th15;
take [p`1,d]~, p9 = p, q9= [p`2,d];
thus u = p9~ by A1;
q ## q9 by A3;
hence v = q9~ by A2,Th27;
thus p9`2 = q9`1;
thus thesis;
end;
uniqueness by Th33;
end;
:: E. ATLAS
theorem Th34:
ex b st u = [a,b]~
proof
consider p such that
A1: u = p~ by Def7;
consider b such that
A2: p`1,p`2 @@ a,b by Th15;
[p`1,p`2] ## [a,b] by A2;
then p ## [a,b];
then p~ = [a,b]~ by Th27;
hence thesis by A1;
end;
definition
let M,a,b;
func vect(a,b) -> Vector of M equals
[a,b]~;
coherence;
end;
theorem Th35:
ex b st u = vect(a,b)
proof
consider b such that
A1: u = [a,b]~ by Th34;
u = vect(a,b) by A1;
hence thesis;
end;
theorem
[a,b] ## [c,d] implies vect(a,b) = vect(c,d) by Th27;
theorem
vect(a,b) = vect(c,d) implies a@d = b@c by Th29;
theorem
ID(M) = vect(b,b) by Th32;
theorem
vect(a,b) = vect(a,c) implies b = c
proof
assume vect(a,b) = vect(a,c);
then a,b @@ a,b & a,b @@ a,c by Th20,Th28;
hence thesis by Th16;
end;
theorem Th40:
vect(a,b) + vect(b,c) = vect(a,c)
proof
set p = [a,b], q = [b,c];
set u = p~, v = q~;
p`2 = b
.= q`1;
then q`2 = c & u + v = [p`1,q`2]~ by Def9;
hence thesis;
end;
:: F. VECTOR GROUPS
theorem Th41:
[a,a@b] ## [a@b,b]
proof
a@b = (a@b)@(a@b) by Def3;
then a,a@b @@ a@b,b;
hence thesis;
end;
theorem
vect(a,a@b) + vect(a,a@b) = vect(a,b)
proof
vect(a,a@b) + vect(a,a@b) = vect(a,a@b) + vect(a@b,b) by Th27,Th41
.= vect(a,b) by Th40;
hence thesis;
end;
theorem Th43:
(u+v)+w = u+(v+w)
proof
set a = the Element of M;
consider b such that
A1: u = vect(a,b) by Th35;
consider c such that
A2: v = vect(b,c) by Th35;
consider d such that
A3: w = vect(c,d) by Th35;
(u+v)+w = vect(a,c)+w by A1,A2,Th40
.= vect(a,d) by A3,Th40
.= vect(a,b)+vect(b,d) by Th40
.= u+(v+w) by A1,A2,A3,Th40;
hence thesis;
end;
theorem Th44:
u+ID(M) = u
proof
set a = the Element of M;
consider b such that
A1: u = vect(a,b) by Th35;
u+ID(M) = vect(a,b)+vect(b,b) by A1,Th32
.= u by A1,Th40;
hence thesis;
end;
theorem Th45:
ex v st u+v = ID(M)
proof
set a = the Element of M;
consider b such that
A1: u = vect(a,b) by Th35;
u + vect(b,a) = vect(a,a) by A1,Th40
.= ID(M) by Th32;
hence thesis;
end;
theorem Th46:
u+v = v+u
proof
set a = the Element of M;
consider b such that
A1: u = vect(a,b) by Th35;
consider c such that
A2: v = vect(b,c) by Th35;
consider d such that
A3: v = vect(a,d) by Th35;
consider c9 such that
A4: u = vect(d,c9) by Th35;
A5: a@c9 = b@d by A1,A4,Th29
.= a@c by A2,A3,Th29;
u + v = vect(a,c) by A1,A2,Th40
.= vect(a,c9) by A5,Th8
.= v + u by A3,A4,Th40;
hence thesis;
end;
theorem Th47:
u + v = u + w implies v = w
proof
assume
A1: u + v = u + w;
consider u9 such that
A2: u + u9 = ID(M) by Th45;
v = v + ID(M) by Th44
.= (u + u9) + v by A2,Th46
.= (u9 + u) + v by Th46
.= u9 + (u + w) by A1,Th43
.= (u9 + u) + w by Th43
.= ID(M) + w by A2,Th46
.= w + ID(M) by Th46;
hence thesis by Th44;
end;
definition
let M,u;
func -u -> Vector of M means
u + it = ID(M);
existence by Th45;
uniqueness by Th47;
end;
reserve X for Subset of [:the carrier of M,the carrier of M:];
definition
let M;
func setvect(M) -> set equals
{ X : X is Vector of M};
coherence;
end;
reserve x for set;
theorem Th48:
x is Vector of M iff x in setvect(M)
proof
thus x is Vector of M implies x in setvect(M);
thus x in setvect(M) implies x is Vector of M
proof
assume x in setvect(M);
then ex X st x = X & X is Vector of M;
hence thesis;
end;
end;
registration
let M;
cluster setvect(M) -> non empty;
coherence
proof
ID(M) in setvect(M);
hence thesis;
end;
end;
reserve u1,v1,w1,W,W1,W2,T for Element of setvect(M);
definition
let M,u1,v1;
func u1 + v1 -> Element of setvect(M) means
:Def13:
for u,v holds u1 = u & v1 = v implies it = u + v;
existence
proof
reconsider u2 = u1, v2 = v1 as Vector of M by Th48;
reconsider suma = u2 + v2 as Element of setvect(M) by Th48;
take suma;
thus thesis;
end;
uniqueness
proof
reconsider u = u1, v = v1 as Vector of M by Th48;
let W1,W2 such that
A1: for u,v holds u1 = u & v1 = v implies W1 = u + v and
A2: for u,v holds u1 = u & v1 = v implies W2 = u + v;
W1 = u + v by A1;
hence thesis by A2;
end;
end;
theorem Th49:
u1 + v1 = v1 + u1
proof
reconsider u = u1, v = v1 as Vector of M by Th48;
thus u1 + v1 = u + v by Def13
.= v + u by Th46
.= v1 + u1 by Def13;
end;
theorem Th50:
(u1 + v1) + w1 = u1 + (v1 + w1)
proof
reconsider u = u1, v = v1, w = w1 as Vector of M by Th48;
A1: v1 + w1 = v + w by Def13;
u1 + v1 = u + v by Def13;
hence (u1 + v1) + w1 = (u + v) + w by Def13
.= u + (v + w) by Th43
.= u1 + (v1 + w1) by A1,Def13;
end;
definition
let M;
func addvect(M) -> BinOp of setvect(M) means
:Def14:
for u1,v1 holds it.(u1, v1) = u1 + v1;
existence
proof
defpred P[Element of setvect(M),Element of setvect(M), Element of setvect(
M)] means $3 = $1 + $2;
A1: for u1,v1 ex W st P[u1,v1,W];
consider o being BinOp of setvect(M) such that
A2: for u1,v1 holds P[u1,v1,o.(u1,v1)] from BINOP_1:sch 3(A1);
take o;
thus thesis by A2;
end;
uniqueness
proof
let f,g be BinOp of setvect(M) such that
A3: for u1,v1 holds f.(u1,v1) = u1 + v1 and
A4: for u1,v1 holds g.(u1,v1) = u1 + v1;
for u1,v1 holds f.(u1,v1) = g.(u1,v1)
proof
let u1,v1;
f.(u1,v1) = u1 + v1 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th51:
for W ex T st W + T = ID(M)
proof
let W;
reconsider x = W as Vector of M by Th48;
consider y being Vector of M such that
A1: x + y = ID(M) by Th45;
reconsider T = y as Element of setvect(M) by Th48;
x + y = W + T by Def13;
hence thesis by A1;
end;
theorem Th52:
for W,W1,W2 st W + W1 = ID(M) & W + W2 = ID(M) holds W1 = W2
proof
let W,W1,W2 such that
A1: W + W1 = ID(M) & W + W2 = ID(M);
reconsider x = W,y1 = W1,y2 = W2 as Vector of M by Th48;
x + y1 = W + W2 by A1,Def13
.= x + y2 by Def13;
hence thesis by Th47;
end;
definition
let M;
func complvect(M) -> UnOp of setvect(M) means
:Def15:
for W holds W + it.W = ID(M);
existence
proof
defpred Z[Element of setvect(M),Element of setvect(M)] means $1 + $2 = ID(
M);
A1: for W ex T st Z[W,T] by Th51;
consider o being UnOp of setvect(M) such that
A2: for W holds Z[W,o.W] from FUNCT_2:sch 3(A1);
take o;
thus thesis by A2;
end;
uniqueness
proof
let f,g be UnOp of setvect(M) such that
A3: ( for W holds W + f.W = ID(M))& for W holds W + g.W = ID(M);
for W holds f.W = g.W
proof
let W;
W + f.W = ID(M) & W + g.W = ID(M) by A3;
hence thesis by Th52;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let M;
func zerovect(M) -> Element of setvect(M) equals
ID(M);
coherence by Th48;
end;
definition
let M;
func vectgroup(M) -> addLoopStr equals
addLoopStr (# setvect(M), addvect(M),
zerovect(M) #);
coherence;
end;
registration
let M;
cluster vectgroup M -> strict non empty;
coherence;
end;
theorem
the carrier of vectgroup(M) = setvect(M);
theorem
the addF of vectgroup(M) = addvect(M);
theorem
0.vectgroup(M) = zerovect M;
theorem
vectgroup(M) is add-associative right_zeroed right_complementable Abelian
proof
set GS = vectgroup(M);
thus GS is add-associative
proof
let x,y,z be Element of GS;
reconsider xx = x, yy = y, zz = z as Element of setvect(M);
thus (x+y)+z = (addvect(M)).(xx+yy,zz) by Def14
.= (xx+yy)+zz by Def14
.= xx+(yy+zz) by Th50
.= (addvect(M)).(xx,yy+zz) by Def14
.= x+(y+z) by Def14;
end;
thus GS is right_zeroed
proof
let x be Element of GS;
reconsider xx = x as Element of setvect(M);
thus x+0.GS = x
proof
reconsider xxx = xx as Vector of M by Th48;
xx+(zerovect(M)) = xxx+ID(M) by Def13
.= x by Th44;
hence thesis by Def14;
end;
end;
thus GS is right_complementable
proof
let x be Element of GS;
reconsider xx = x as Element of setvect(M);
reconsider w = (complvect(M)).xx as Element of GS;
take w;
thus x + w = xx + (complvect(M)).xx by Def14
.= 0.GS by Def15;
end;
thus GS is Abelian
proof
let x,y be Element of GS;
reconsider xx = x, yy = y as Element of setvect(M);
thus x+y = xx + yy by Def14
.= yy + xx by Th49
.= y+x by Def14;
end;
end;