:: Midpoint algebras :: by Micha{\l} Muzalewski :: :: Received November 26, 1989 :: Copyright (c) 1990-2018 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;