:: Groups :: by Wojciech A. Trybulec :: :: Received July 3, 1990 :: Copyright (c) 1990-2021 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 NUMBERS, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2, RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1, SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1, TARSKI, RLVECT_1, SUPINF_2, GROUP_1, ORDINAL1; notations TARSKI, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, INT_1, NAT_1, FINSEQOP, SETWISEO, INT_2; constructors BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2, FINSEQOP, RLVECT_1; registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, STRUCT_0, ALGSTR_0, CARD_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve m,n for Nat; reserve i,j for Integer; reserve S for non empty multMagma; reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S; definition let IT be multMagma; attr IT is unital means :: GROUP_1:def 1 ex e being Element of IT st for h being Element of IT holds h * e = h & e * h = h; attr IT is Group-like means :: GROUP_1:def 2 ex e being Element of IT st for h being Element of IT holds h * e = h & e * h = h & ex g being Element of IT st h * g = e & g * h = e; attr IT is associative means :: GROUP_1:def 3 for x,y,z being Element of IT holds (x*y )*z = x*(y*z); end; registration cluster Group-like -> unital for multMagma; end; registration cluster strict Group-like associative non empty for multMagma; end; definition mode Group is Group-like associative non empty multMagma; end; theorem :: GROUP_1:1 ((for r,s,t holds (r * s) * t = r * (s * t)) & ex t st for s1 holds s1 * t = s1 & t * s1 = s1 & ex s2 st s1 * s2 = t & s2 * s1 = t) implies S is Group ; theorem :: GROUP_1:2 (for r,s,t holds r * s * t = r * (s * t)) & (for r,s holds (ex t st r * t = s) & (ex t st t * r = s)) implies S is associative Group-like; theorem :: GROUP_1:3 multMagma (# REAL, addreal #) is associative Group-like; reserve G for Group-like non empty multMagma; reserve e,h for Element of G; definition let G be multMagma such that G is unital; func 1_G -> Element of G means :: GROUP_1:def 4 for h being Element of G holds h * it = h & it * h = h; end; theorem :: GROUP_1:4 (for h holds h * e = h & e * h = h) implies e = 1_G; reserve G for Group; reserve f,g,h for Element of G; definition let G,h; func h" -> Element of G means :: GROUP_1:def 5 h * it = 1_G & it * h = 1_G; involutiveness; end; theorem :: GROUP_1:5 h * g = 1_G & g * h = 1_G implies g = h"; theorem :: GROUP_1:6 h * g = h * f or g * h = f * h implies g = f; theorem :: GROUP_1:7 h * g = h or g * h = h implies g = 1_G; theorem :: GROUP_1:8 (1_G)" = 1_G; theorem :: GROUP_1:9 h" = g" implies h = g; theorem :: GROUP_1:10 h" = 1_G implies h = 1_G; ::$CT theorem :: GROUP_1:12 h * g = 1_G implies h = g" & g = h"; theorem :: GROUP_1:13 h * f = g iff f = h" * g; theorem :: GROUP_1:14 f * h = g iff f = g * h"; theorem :: GROUP_1:15 ex f st g * f = h; theorem :: GROUP_1:16 ex f st f * g = h; theorem :: GROUP_1:17 (h * g)" = g" * h"; theorem :: GROUP_1:18 g * h = h * g iff (g * h)" = g" * h"; theorem :: GROUP_1:19 g * h = h * g iff g" * h" = h" * g"; theorem :: GROUP_1:20 g * h = h * g iff g * h" = h" * g; reserve u for UnOp of G; definition let G; func inverse_op(G) -> UnOp of G means :: GROUP_1:def 6 it.h = h"; end; registration let G be associative non empty multMagma; cluster the multF of G -> associative; end; theorem :: GROUP_1:21 for G being unital non empty multMagma holds 1_G is_a_unity_wrt the multF of G; theorem :: GROUP_1:22 for G being unital non empty multMagma holds the_unity_wrt the multF of G = 1_G; registration let G be unital non empty multMagma; cluster the multF of G -> having_a_unity; end; theorem :: GROUP_1:23 inverse_op(G) is_an_inverseOp_wrt the multF of G; registration let G; cluster the multF of G -> having_an_inverseOp; end; theorem :: GROUP_1:24 the_inverseOp_wrt the multF of G = inverse_op(G); definition let G be non empty multMagma; func power G -> Function of [:the carrier of G,NAT:], the carrier of G means :: GROUP_1:def 7 for h being Element of G holds it.(h,0) = 1_G & for n being Nat holds it.(h,n + 1) = it.(h,n) * h; end; definition let G,h; let i be Integer; func h |^ i -> Element of G equals :: GROUP_1:def 8 power(G).(h,|.i.|) if 0 <= i otherwise (power(G).(h,|.i.|))"; end; definition let G,h; let n be natural Number; redefine func h |^ n equals :: GROUP_1:def 9 power(G).(h,n); end; theorem :: GROUP_1:25 h |^ 0 = 1_G; theorem :: GROUP_1:26 h |^ 1 = h; theorem :: GROUP_1:27 h |^ 2 = h * h; theorem :: GROUP_1:28 h |^ 3 = h * h * h; theorem :: GROUP_1:29 h |^ 2 = 1_G iff h" = h; theorem :: GROUP_1:30 i <= 0 implies h |^ i = (h |^ |.i.|)"; theorem :: GROUP_1:31 (1_G) |^ i = 1_G; theorem :: GROUP_1:32 h |^ (-1) = h"; theorem :: GROUP_1:33 h |^ (i + j) = (h |^ i) * (h |^ j); theorem :: GROUP_1:34 h |^ (i + 1) = h |^ i * h & h |^ (i + 1) = h * (h |^ i); theorem :: GROUP_1:35 h |^ (i * j) = h |^ i |^ j; theorem :: GROUP_1:36 h |^ -i = (h |^ i)"; theorem :: GROUP_1:37 h" |^ i = (h |^ i)"; theorem :: GROUP_1:38 g * h = h * g implies (g * h) |^ i = g |^ i * (h |^ i); theorem :: GROUP_1:39 g * h = h * g implies g |^ i * (h |^ j) = h |^ j * (g |^ i); theorem :: GROUP_1:40 g * h = h * g implies g * (h |^ i) = h |^ i * g; definition let G,h; attr h is being_of_order_0 means :: GROUP_1:def 10 h |^ n = 1_G implies n = 0; end; registration let G; cluster 1_G -> non being_of_order_0; end; definition let G,h; func ord h -> Element of NAT means :: GROUP_1:def 11 it = 0 if h is being_of_order_0 otherwise h |^ it = 1_G & it <> 0 & for m st h |^ m = 1_G & m <> 0 holds it <= m; end; theorem :: GROUP_1:41 h |^ ord h = 1_G; theorem :: GROUP_1:42 ord 1_G = 1; theorem :: GROUP_1:43 ord h = 1 implies h = 1_G; theorem :: GROUP_1:44 h |^ n = 1_G implies ord h divides n; definition let G be finite 1-sorted; redefine func card G -> Element of NAT; end; theorem :: GROUP_1:45 for G being non empty finite 1-sorted holds card G >= 1; definition let IT be multMagma; attr IT is commutative means :: GROUP_1:def 12 for x, y being Element of IT holds x*y = y*x; end; registration cluster strict commutative for Group; end; definition let FS be commutative non empty multMagma; let x,y be Element of FS; redefine func x*y; commutativity; end; theorem :: GROUP_1:46 multMagma (# REAL, addreal #) is commutative Group; reserve A for commutative Group; reserve a,b for Element of A; theorem :: GROUP_1:47 (a * b)" = a" * b"; theorem :: GROUP_1:48 (a * b) |^ i = a |^ i * (b |^ i); theorem :: GROUP_1:49 addLoopStr (# the carrier of A, the multF of A, 1_A #) is Abelian add-associative right_zeroed right_complementable; begin :: Addenda :: from COMPTRIG, 2006.08.12, A.T. theorem :: GROUP_1:50 for L be unital non empty multMagma for x be Element of L holds (power L).(x,1) = x; theorem :: GROUP_1:51 for L be unital non empty multMagma for x be Element of L holds (power L).(x,2) = x*x; theorem :: GROUP_1:52 for L be associative commutative unital non empty multMagma for x,y be Element of L for n be Nat holds (power L).(x*y,n) = (power L).(x,n) * (power L).(y,n); :: Moved from ENDALG, 17.01_2006, AK definition let G,H be multMagma; let IT be Function of G,H; attr IT is unity-preserving means :: GROUP_1:def 13 IT.1_G = 1_H; end;