:: Midpoint algebras
:: by Micha{\l} Muzalewski
::
:: Received November 26, 1989
:: Copyright (c) 1990-2016 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;
begin :: PRELIMINARY
definition
struct(1-sorted) MidStr (# carrier -> set, MIDPOINT -> BinOp of the carrier
#);
end;
registration
cluster non empty for MidStr;
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
:: MIDSP_1:def 1
(the MIDPOINT of MS).(a,b);
end;
definition
func Example -> MidStr equals
:: MIDSP_1:def 2
MidStr (# {0}, op2 #);
end;
registration
cluster Example -> strict non 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 :: 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. MIDPOINT ALGEBRAS
definition
let IT be non empty MidStr;
attr IT is MidSp-like means
:: 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;
registration
cluster strict MidSp-like for non empty MidStr;
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;
commutativity;
end;
reserve M for MidSp;
reserve a,b,c,d,a9,b9,c9,d9,x,y,x9 for Element of M;
theorem :: MIDSP_1:5
(a@b)@c = (a@c)@(b@c);
theorem :: MIDSP_1:6 :: right-self-distributivity
a@(b@c) = (a@b)@(a@c);
theorem :: MIDSP_1:7 :: left-self-distributivity
a@b = a implies a = b;
theorem :: MIDSP_1:8
x@a = x9@a implies x = x9;
theorem :: MIDSP_1:9 :: right-cancellation-law
a@x = a@x9 implies x = x9;
:: left-cancellation-law
:: B. CONGRUENCE RELATION
definition
let M,a,b,c,d;
pred a,b @@ c,d means
:: MIDSP_1:def 4 :: bound-vectors ab, cd are equivalent
a@d = b@c;
end;
theorem :: MIDSP_1:10
a,a @@ b,b;
theorem :: MIDSP_1:11
a,b @@ c,d implies c,d @@ a,b;
theorem :: MIDSP_1:12
a,a @@ b,c implies b = c;
theorem :: MIDSP_1:13
a,b @@ c,c implies a = b;
theorem :: MIDSP_1:14
a,b @@ a,b;
theorem :: MIDSP_1:15
ex d st a,b @@ c,d;
theorem :: MIDSP_1:16
a,b @@ c,d & a,b @@ c,d9 implies d = d9;
theorem :: MIDSP_1:17
x,y @@ a,b & x,y @@ c,d implies a,b @@ c,d;
theorem :: MIDSP_1:18
a,b @@ a9,b9 & b,c @@ b9,c9 implies a,c @@ a9,c9;
:: 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
:: MIDSP_1:def 5
p`1,p`2 @@ q`1,q`2;
reflexivity;
symmetry;
end;
theorem :: MIDSP_1:19
a,b @@ c,d implies [a,b] ## [c,d];
theorem :: MIDSP_1:20
[a,b] ## [c,d] implies a,b @@ c,d;
theorem :: MIDSP_1:21
p ## q & p ## r implies q ## r;
theorem :: MIDSP_1:22
p ## r & q ## r implies p ## q;
theorem :: MIDSP_1:23
p ## q & q ## r implies p ## r;
theorem :: MIDSP_1:24
p ## q implies (r ## p iff r ## q);
theorem :: MIDSP_1:25
for p holds { q : q ## p } is non empty Subset of [:the carrier
of M,the carrier of M:];
:: D. ( FREE ) VECTORS
definition
let M,p;
func p~ -> Subset of [:the carrier of M,the carrier of M:] equals
:: MIDSP_1:def 6
{ q : q ## p};
end;
registration
let M,p;
cluster p~ -> non empty;
end;
theorem :: MIDSP_1:26
for p holds r in p~ iff r ## p;
theorem :: MIDSP_1:27
p ## q implies p~ = q~;
theorem :: MIDSP_1:28
p~ = q~ implies p ## q;
theorem :: MIDSP_1:29
[a,b]~ = [c,d]~ implies a@d = b@c;
theorem :: MIDSP_1:30
p in p~;
definition
let M;
mode Vector of M -> non empty Subset of [:the carrier of M,the carrier of M
:] means
:: MIDSP_1:def 7
ex p st it = p~;
end;
reserve u,v,w,u9,w9 for Vector of M;
definition
let M,p;
redefine func p~ -> Vector of M;
end;
theorem :: MIDSP_1:31
ex u st for p holds p in u iff p`1 = p`2;
definition
let M;
func ID(M) -> Vector of M equals
:: MIDSP_1:def 8 :: zero vector
{ p : p`1 = p`2 };
end;
theorem :: MIDSP_1:32
ID(M) = [b,b]~;
theorem :: MIDSP_1:33
(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;
definition
let M,u,v;
func u + v -> Vector of M means
:: MIDSP_1:def 9
ex p,q st u = p~ & v = q~ & p`2 = q `1 & it = [p`1,q`2]~;
end;
:: E. ATLAS
theorem :: MIDSP_1:34
ex b st u = [a,b]~;
definition
let M,a,b;
func vect(a,b) -> Vector of M equals
:: MIDSP_1:def 10
[a,b]~;
end;
theorem :: MIDSP_1:35
ex b st u = vect(a,b);
theorem :: MIDSP_1:36
[a,b] ## [c,d] implies vect(a,b) = vect(c,d);
theorem :: MIDSP_1:37
vect(a,b) = vect(c,d) implies a@d = b@c;
theorem :: MIDSP_1:38
ID(M) = vect(b,b);
theorem :: MIDSP_1:39
vect(a,b) = vect(a,c) implies b = c;
theorem :: MIDSP_1:40
vect(a,b) + vect(b,c) = vect(a,c);
:: F. VECTOR GROUPS
theorem :: MIDSP_1:41
[a,a@b] ## [a@b,b];
theorem :: MIDSP_1:42
vect(a,a@b) + vect(a,a@b) = vect(a,b);
theorem :: MIDSP_1:43
(u+v)+w = u+(v+w);
theorem :: MIDSP_1:44
u+ID(M) = u;
theorem :: MIDSP_1:45
ex v st u+v = ID(M);
theorem :: MIDSP_1:46
u+v = v+u;
theorem :: MIDSP_1:47
u + v = u + w implies v = w;
definition
let M,u;
func -u -> Vector of M means
:: MIDSP_1:def 11
u + it = ID(M);
end;
reserve X for Subset of [:the carrier of M,the carrier of M:];
definition
let M;
func setvect(M) -> set equals
:: MIDSP_1:def 12
{ X : X is Vector of M};
end;
reserve x for set;
theorem :: MIDSP_1:48
x is Vector of M iff x in setvect(M);
registration
let M;
cluster setvect(M) -> non empty;
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
:: MIDSP_1:def 13
for u,v holds u1 = u & v1 = v implies it = u + v;
end;
theorem :: MIDSP_1:49
u1 + v1 = v1 + u1;
theorem :: MIDSP_1:50
(u1 + v1) + w1 = u1 + (v1 + w1);
definition
let M;
func addvect(M) -> BinOp of setvect(M) means
:: MIDSP_1:def 14
for u1,v1 holds it.(u1, v1) = u1 + v1;
end;
theorem :: MIDSP_1:51
for W ex T st W + T = ID(M);
theorem :: MIDSP_1:52
for W,W1,W2 st W + W1 = ID(M) & W + W2 = ID(M) holds W1 = W2;
definition
let M;
func complvect(M) -> UnOp of setvect(M) means
:: MIDSP_1:def 15
for W holds W + it.W = ID(M);
end;
definition
let M;
func zerovect(M) -> Element of setvect(M) equals
:: MIDSP_1:def 16
ID(M);
end;
definition
let M;
func vectgroup(M) -> addLoopStr equals
:: MIDSP_1:def 17
addLoopStr (# setvect(M), addvect(M),
zerovect(M) #);
end;
registration
let M;
cluster vectgroup M -> strict non empty;
end;
theorem :: MIDSP_1:53
the carrier of vectgroup(M) = setvect(M);
theorem :: MIDSP_1:54
the addF of vectgroup(M) = addvect(M);
theorem :: MIDSP_1:55
0.vectgroup(M) = zerovect M;
theorem :: MIDSP_1:56
vectgroup(M) is add-associative right_zeroed right_complementable Abelian;