From 65d6f8d6c9e98511d2048371fa049610c73b1960 Mon Sep 17 00:00:00 2001 From: avekens Date: Sat, 13 Jan 2024 11:16:18 +0100 Subject: [PATCH] Theorems about magmas, semigroups and monoids (continued) Subsection "Identity elements": * ~grprinvlem, ~grprinvd, ~grpridd moved from subsection "Operations" * ~lidrididd ~lidrideqd moved from AV's mathbox to main Subsection "Iterated sums in a magma": * ~gsumsplit1r moved from AV's mathbox to main Subsection "Definition and basic properties of monoids": * ~mndbn0 moved from AV's mathbox to main * proofs of ~slmdbn0 , ~slmdsn0 in TA's mathbox shortened Subsection "Iterated sums in a monoid": * ~gsumsgrpccat moved from AV's mathbox to main * proof of ~gsumccat shortened Subsection "Group multiple operation": * ~mulgnn0gsum, ~mulgnngsum moved from AV's mathbox to main New subsection "Cyclic monoids and groups": * ~cycsubgcl, ~cycsubgss, ~cycsubg, ~cycsubg2, ~cycsubg2cl, ~cycsubggend, ~cycsubgcld moved from other places * ~cycsubm ~cycsubmcl ~cycsubmel moved from AV's mathbox to main New subsection header "Direct products (extension)": * ~smndlsmidm, ~mndlsmidm moved from AV's mathbox to main * proof of ~lsmidm shortened Subsection "Abelian groups": * new theorem ~invmod (variant of ~caovmo) added Subsubsection "Group sum operation" * ~gsumreidx, ~gsumxp2 moved from AV's mathbox to main * ~gsumcom3, ~gsumcom3fi moved up from section "Matrix multiplication" Miscellaneous: * ~gcdmultiplez, ~gcdmultiple moved up and proofs shortened * Header for subsubsection "Definition and basic properties" of subsection "Simple groups" added * Header for subsubsection "Convert operation laws using setvar variables to class notation" of subsection "Operations" added --- changes-set.txt | 14 + discouraged | 10 +- set.mm | 1107 +++++++++++++++++++++++++---------------------- 3 files changed, 606 insertions(+), 525 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 8429b4cad6..0be996339c 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -81,6 +81,20 @@ make a github issue.) DONE: Date Old New Notes +13-Jan-24 mndlsmidm [same] moved from AV's mathbox to main set.mm +13-Jan-24 smndlsmidm [same] moved from AV's mathbox to main set.mm +13-Jan-24 cycsubm [same] moved from AV's mathbox to main set.mm +13-Jan-24 cycsubmcl [same] moved from AV's mathbox to main set.mm +13-Jan-24 cycsubmel [same] moved from AV's mathbox to main set.mm +13-Jan-24 mulgnn0gsum [same] moved from AV's mathbox to main set.mm +13-Jan-24 mulgnngsum [same] moved from AV's mathbox to main set.mm +13-Jan-24 gsumxp2 [same] moved from AV's mathbox to main set.mm +13-Jan-24 gsumreidx [same] moved from AV's mathbox to main set.mm +13-Jan-24 gsumsgrpccat [same] moved from AV's mathbox to main set.mm +13-Jan-24 gsumsplit1r [same] moved from AV's mathbox to main set.mm +13-Jan-24 mndbn0 [same] moved from AV's mathbox to main set.mm +13-Jan-24 lidrididd [same] moved from AV's mathbox to main set.mm +13-Jan-24 lidrideqd [same] moved from AV's mathbox to main set.mm 5-Jan-24 --- --- sections "Groups" and "Simple groups" moved from RR's mathbox to main set.mm 5-Jan-24 rr-php2d phpeqd moved from RR's mathbox to main set.mm diff --git a/discouraged b/discouraged index 0d16ed03da..5ffe0c6764 100755 --- a/discouraged +++ b/discouraged @@ -15266,6 +15266,8 @@ New usage of "fvsnOLD" is discouraged (0 uses). New usage of "fvsngOLD" is discouraged (0 uses). New usage of "fvsnun1OLD" is discouraged (0 uses). New usage of "fvsnun2OLD" is discouraged (0 uses). +New usage of "gcdmultipleOLD" is discouraged (0 uses). +New usage of "gcdmultiplezOLD" is discouraged (0 uses). New usage of "gen11" is discouraged (19 uses). New usage of "gen11nv" is discouraged (5 uses). New usage of "gen12" is discouraged (7 uses). @@ -15349,6 +15351,7 @@ New usage of "grporndm" is discouraged (4 uses). New usage of "grposnOLD" is discouraged (1 uses). New usage of "grpplusgx" is discouraged (3 uses). New usage of "grpsubfvalALT" is discouraged (0 uses). +New usage of "gsumccatOLD" is discouraged (0 uses). New usage of "gt-lt" is discouraged (0 uses). New usage of "gt-lth" is discouraged (1 uses). New usage of "gt0srpr" is discouraged (2 uses). @@ -16105,6 +16108,7 @@ New usage of "lsatfixedN" is discouraged (1 uses). New usage of "lshpinN" is discouraged (0 uses). New usage of "lshpnel2N" is discouraged (0 uses). New usage of "lshpset2N" is discouraged (1 uses). +New usage of "lsmidmOLD" is discouraged (0 uses). New usage of "ltaddnq" is discouraged (7 uses). New usage of "ltaddpr" is discouraged (5 uses). New usage of "ltaddpr2" is discouraged (1 uses). @@ -18765,6 +18769,8 @@ Proof modification of "fvsnOLD" is discouraged (28 steps). Proof modification of "fvsngOLD" is discouraged (86 steps). Proof modification of "fvsnun1OLD" is discouraged (124 steps). Proof modification of "fvsnun2OLD" is discouraged (112 steps). +Proof modification of "gcdmultipleOLD" is discouraged (348 steps). +Proof modification of "gcdmultiplezOLD" is discouraged (230 steps). Proof modification of "gen11" is discouraged (27 steps). Proof modification of "gen11nv" is discouraged (14 steps). Proof modification of "gen12" is discouraged (16 steps). @@ -18779,7 +18785,7 @@ Proof modification of "ghomlinOLD" is discouraged (161 steps). Proof modification of "grpinvfvalALT" is discouraged (161 steps). Proof modification of "grposnOLD" is discouraged (291 steps). Proof modification of "grpsubfvalALT" is discouraged (189 steps). -Proof modification of "gsumccatNEW" is discouraged (310 steps). +Proof modification of "gsumccatOLD" is discouraged (994 steps). Proof modification of "hadcomaOLD" is discouraged (37 steps). Proof modification of "hashge3el3dif" is discouraged (229 steps). Proof modification of "hba1-o" is discouraged (34 steps). @@ -18872,7 +18878,7 @@ Proof modification of "latmassOLD" is discouraged (309 steps). Proof modification of "lcmftp" is discouraged (1057 steps). Proof modification of "lediv2aALT" is discouraged (264 steps). Proof modification of "leibpilem1OLD" is discouraged (254 steps). -Proof modification of "lsmidmNEW" is discouraged (25 steps). +Proof modification of "lsmidmOLD" is discouraged (116 steps). Proof modification of "luk-1" is discouraged (73 steps). Proof modification of "luk-2" is discouraged (52 steps). Proof modification of "luk-3" is discouraged (20 steps). diff --git a/set.mm b/set.mm index d5608d2bda..1bdfe4a07b 100644 --- a/set.mm +++ b/set.mm @@ -68486,6 +68486,13 @@ result of an operator (deduction version). (Contributed by Paul BDMZUCUAEKZTUCUEUBEKUAUBEEDHNOUETAEKCAEFGIPOQTUDUCJRS $. $} + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Convert operation laws using setvar variables to class notation +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + ${ $d x y A $. $d y B $. $d x y C $. $d x y D $. $d x y E $. $d x y ph $. $d x y F $. @@ -69001,65 +69008,6 @@ result of an operator (deduction version). (Contributed by Paul $} $} - ${ - $d n u v w x y z B $. $d n u v w x y z O $. $d n u v w x y z ph $. - $d u v w y z N $. $d n u v w x y z .+ $. $d u v w y z X $. - $d u v w y ps $. - grprinvlem.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) $. - grprinvlem.o $e |- ( ph -> O e. B ) $. - grprinvlem.i $e |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x ) $. - grprinvlem.a $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) - -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) $. - grprinvlem.n $e |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O ) $. - ${ - grprinvlem.x $e |- ( ( ph /\ ps ) -> X e. B ) $. - grprinvlem.e $e |- ( ( ph /\ ps ) -> ( X .+ X ) = X ) $. - $( Lemma for ~ grprinvd . (Contributed by NM, 9-Aug-2013.) $) - grprinvlem $p |- ( ( ph /\ ps ) -> X = O ) $= - ( cv co wceq wcel vu vv vw wa wrex wral ralrimiva oveq2 rexbidv cbvralv - eqeq1d sylib syl2an2r oveq2d adantr simprr oveq1d w3a caovassg ad4ant14 - rspccva simprl caovassd id eqeq12d rspcdva 3eqtr3d rexlimddv ) ABUDZDQZ - IGRZHSZIHSDFAVJEQZGRZHSZDFUEZEFUFZBIFTZVLDFUEZAVJCQZGRZHSZDFUEZCFUFVQAW - CCFNUGWCVPCEFVTVMSZWBVODFWDWAVNHVTVMVJGUHUKUIUJULOVPVSEIFVMISZVOVLDFWEV - NVKHVMIVJGUHUKUIVAUMVIVJFTZVLUDZUDZVJIIGRZGRZVKIHVIWJVKSWGVIWIIVJGPUNUO - WHVKIGRHIGRZWJIWHVKHIGVIWFVLUPZUQWHUAUBUCVJIIFGAUAQZFTUBQZFTUCQZFTURWMW - NGRWOGRWMWNWOGRGRSBWGACDEWMWNWOFGMUSUTVIWFVLVBVIVRWGOUOZWPVCVIWKISZWGVI - HVJGRZVJSZWQDFIVJISZWRWKVJIVJIHGUHWTVDVEAWSDFUFZBAHVTGRZVTSZCFUFXAAXCCF - LUGXCWSCDFVTVJSZXBWRVTVJVTVJHGUHXDVDVEUJULUOOVFUOVGWLVGVH $. - $} - - ${ - grprinvd.x $e |- ( ( ph /\ ps ) -> X e. B ) $. - grprinvd.n $e |- ( ( ph /\ ps ) -> N e. B ) $. - grprinvd.e $e |- ( ( ph /\ ps ) -> ( N .+ X ) = O ) $. - $( Deduce right inverse from left inverse and left identity in an - associative structure (such as a group). (Contributed by NM, - 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) $) - grprinvd $p |- ( ( ph /\ ps ) -> ( X .+ N ) = O ) $= - ( co wcel vu vv vw wa cv caovclg adantlr caovcld wceq caovassg caovassd - 3expb w3a oveq1d oveq2 id eqeq12d wral ralrimiva cbvralv adantr rspcdva - sylib 3eqtr3d oveq2d eqtrd grprinvlem ) ABCDEFGIJHGSZKLMNOABUDZUAUBJHFF - FGAUAUEZFTZUBUEZFTZUDVJVLGSZFTBACDVJVLFFFGACUEZFTDUEZFTVOVPGSFTKULUFUGP - QUHZVIVHVHGSJHVHGSZGSVHVIUAUBUCJHVHFGAVKVMUCUEZFTUMVNVSGSVJVLVSGSGSUIBA - CDEVJVLVSFGNUJUGZPQVQUKVIVRHJGVIHJGSZHGSIHGSZVRHVIWAIHGRUNVIUAUBUCHJHFG - VTQPQUKVIIVPGSZVPUIZWBHUIDFHVPHUIZWCWBVPHVPHIGUOWEUPUQAWDDFURZBAIVOGSZV - OUIZCFURWFAWHCFMUSWHWDCDFVOVPUIZWGWCVOVPVOVPIGUOWIUPUQUTVCVAQVBVDVEVFVG - $. - $} - - $( Deduce right identity from left inverse and left identity in an - associative structure (such as a group). (Contributed by NM, - 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) $) - grpridd $p |- ( ( ph /\ x e. B ) -> ( x .+ O ) = x ) $= - ( vn vu vv cv wcel wa co wceq vw wrex oveq1 eqeq1d cbvrexv sylib caovassg - w3a adantlr simprl simprrl caovassd simprrr oveq1d oveq2d 3eqtr3d anassrs - grprinvd rexlimddv eqtr3d ) ABPZEQZRZGVAFSZVAGFSZVAVCMPZVAFSZGTZVDVETZMEV - CCPZVAFSZGTZCEUBVHMEUBLVLVHCMEVJVFTVKVGGVJVFVAFUCUDUEUFAVBVFEQZVHRZVIAVBV - NRZRZVAVFFSZVAFSVAVGFSVDVEVPNOUAVAVFVAEFANPZEQOPZEQUAPZEQUHVRVSFSVTFSVRVS - VTFSFSTVOABCDVRVSVTEFKUGUIAVBVNUJZAVBVMVHUKZWAULVPVQGVAFAVOBCDEFVFGVAHIJK - LWAWBAVBVMVHUMZURUNVPVGGVAFWCUOUPUQUSJUT $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -180211,6 +180159,24 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact CKLBKLFKLUFUIMEABDNZAOCBFPQABSLUFBMDBRTAUHUGBGAUGAUGACBEUJUAUBUCUDUE $. $} + $( The GCD of a multiple of an integer is the integer itself. (Contributed + by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) + (Proof shortened by AV, 12-Jan-2023.) $) + gcdmultiplez $p |- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M ) $= + ( cn wcel cz wa cmul co cgcd cc nncn adantr zcn adantl mulcomd oveq2d nnnn0 + cn0 simpr gcdmultipled eqtrd ) ACDZBEDZFZAABGHZIHABAGHZIHAUDUEUFAIUDABUBAJD + UCAKLUCBJDUBBMNOPUDABUBARDUCAQLUBUCSTUA $. + + ${ + $d M k n $. $d N k n $. + $( The GCD of a multiple of a positive integer is the positive integer + itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario + Carneiro, 19-Apr-2014.) (Proof shortened by AV, 12-Jan-2023.) $) + gcdmultiple $p |- ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M ) $= + ( cn wcel cz cmul co cgcd wceq nnz gcdmultiplez sylan2 ) BCDACDBEDAABFGHG + AIBJABKL $. + $} + ${ dvdsgcdidd.1 $e |- ( ph -> M e. NN ) $. dvdsgcdidd.2 $e |- ( ph -> N e. ZZ ) $. @@ -180567,10 +180533,12 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact ${ $d M k n $. $d N k n $. - $( The GCD of a multiple of a number is the number itself. (Contributed by - Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, - 19-Apr-2014.) $) - gcdmultiple $p |- ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M ) $= + $( Obsolete proof of ~ gcdmultiple as of 12-Jan-2024. The GCD of a + multiple of a number is the number itself. (Contributed by Scott + Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + gcdmultipleOLD $p |- ( ( M e. NN /\ N e. NN ) + -> ( M gcd ( M x. N ) ) = M ) $= ( vk vn cn wcel cmul co cgcd wi c1 caddc oveq2 oveq2d eqeq1d imbi2d eqtrd wceq cz cc cv weq nncn mulid1d cabs cfv nnz gcdid syl nnre nn0ge0d absidd nnnn0 wa zmulcl syl2an gcdaddm mp3an2ani ax-1cn adddi mp3an3 mulcom mpan2 @@ -180585,9 +180553,12 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact BVCVENQUPNVFOVGVHVIVJVK $. $} - $( Extend ~ gcdmultiple so ` N ` can be an integer. (Contributed by Scott - Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) $) - gcdmultiplez $p |- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M ) $= + $( Obsolete proof of ~ gcdmultiple as of 12-Jan-2024. Extend ~ gcdmultiple + so ` N ` can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) + (Revised by Mario Carneiro, 19-Apr-2014.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + gcdmultiplezOLD $p |- ( ( M e. NN /\ N e. ZZ ) + -> ( M gcd ( M x. N ) ) = M ) $= ( cn wcel cz wa cmul co cgcd wceq cc0 oveq2 oveq2d eqeq1d cabs cfv cc eqtrd adantr syl wne nncn zcn absmul syl2an nnre nnnn0 nn0ge0d absidd oveq1d nnzd simpll nnz zmulcl sylan gcdabs2 syl2anc nnabscl gcdmultiple anassrs 3eqtr3d @@ -215215,6 +215186,40 @@ is an important property of monoids (see ~ mndid ), and therefore also for USVCURNECVBUOBUMUTUMDCEUTERVAUNUMUTEUMDUCUDUEUFUHUIUJUK $. $} + ${ + $d B x $. $d L x $. $d R x $. $d .+ x $. + lidrideqd.l $e |- ( ph -> L e. B ) $. + lidrideqd.r $e |- ( ph -> R e. B ) $. + lidrideqd.li $e |- ( ph -> A. x e. B ( L .+ x ) = x ) $. + lidrideqd.ri $e |- ( ph -> A. x e. B ( x .+ R ) = x ) $. + $( If there is a left and right identity element for any binary operation + (group operation) ` .+ ` , both identity elements are equal. + Generalization of statement in [Lang] p. 3: it is sufficient that "e" is + a left identity element and "e``" is a right identity element instead of + both being (two-sided) identity elements. (Contributed by AV, + 26-Dec-2023.) $) + lidrideqd $p |- ( ph -> L = R ) $= + ( co cv wceq oveq1 id eqeq12d rspcdva oveq2 eqtr3d ) AFEDKZFEABLZEDKZUAMT + FMBCFUAFMZUBTUAFUAFEDNUCOPJGQAFUADKZUAMTEMBCEUAEMZUDTUAEUAEFDRUEOPIHQS $. + + $d B x y $. $d L y $. $d R y $. $d G y $. $d .+ y $. $d .0. y $. + $d ph y $. + lidrideqd.b $e |- B = ( Base ` G ) $. + lidrideqd.p $e |- .+ = ( +g ` G ) $. + lidrididd.o $e |- .0. = ( 0g ` G ) $. + $( If there is a left and right identity element for any binary operation + (group operation) ` .+ ` , the left identity element (and therefore also + the right identity element according to ~ lidrideqd ) is equal to the + two-sided identity element. (Contributed by AV, 26-Dec-2023.) $) + lidrididd $p |- ( ph -> L = .0. ) $= + ( vy cv co wceq wral wcel oveq2 id eqeq12d rspcv mpan9 wi lidrideqd oveq1 + weq wa adantl simpl eqtrd ex syl6com com23 sylc imp ismgmid2 ) APCDGFHMON + IAGBQZDRZVASZBCTPQZCUAZGVDDRZVDSZKVCVGBVDCBPUJZVBVFVAVDVAVDGDUBVHUCZUDUEU + FAVEVDGDRZVDSZAVAEDRZVASZBCTZGESZVEVKUGLABCDEGIJKLUHVNVEVOVKVEVNVDEDRZVDS + ZVOVKUGVMVQBVDCVHVLVPVAVDVAVDEDUIVIUDUEVQVOVKVQVOUKVJVPVDVOVJVPSVQGEVDDUB + ULVQVOUMUNUOUPUQURUSUT $. + $} + ${ $d x G $. $d x ph $. $d x .0. $. grpidd.b $e |- ( ph -> B = ( Base ` G ) ) $. @@ -215251,6 +215256,65 @@ is an important property of monoids (see ~ mndid ), and therefore also for IUGUJUKULUMUNAHUOTUPUSVEACVGUQTUR $. $} + ${ + $d n u v w x y z B $. $d n u v w x y z O $. $d n u v w x y z ph $. + $d u v w y z N $. $d n u v w x y z .+ $. $d u v w y z X $. + $d u v w y ps $. + grprinvlem.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) $. + grprinvlem.o $e |- ( ph -> O e. B ) $. + grprinvlem.i $e |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x ) $. + grprinvlem.a $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) + -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) $. + grprinvlem.n $e |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O ) $. + ${ + grprinvlem.x $e |- ( ( ph /\ ps ) -> X e. B ) $. + grprinvlem.e $e |- ( ( ph /\ ps ) -> ( X .+ X ) = X ) $. + $( Lemma for ~ grprinvd . (Contributed by NM, 9-Aug-2013.) $) + grprinvlem $p |- ( ( ph /\ ps ) -> X = O ) $= + ( cv co wceq wcel vu vv vw wa wrex wral ralrimiva oveq2 rexbidv cbvralv + eqeq1d sylib syl2an2r oveq2d adantr simprr oveq1d w3a caovassg ad4ant14 + rspccva simprl caovassd id eqeq12d rspcdva 3eqtr3d rexlimddv ) ABUDZDQZ + IGRZHSZIHSDFAVJEQZGRZHSZDFUEZEFUFZBIFTZVLDFUEZAVJCQZGRZHSZDFUEZCFUFVQAW + CCFNUGWCVPCEFVTVMSZWBVODFWDWAVNHVTVMVJGUHUKUIUJULOVPVSEIFVMISZVOVLDFWEV + NVKHVMIVJGUHUKUIVAUMVIVJFTZVLUDZUDZVJIIGRZGRZVKIHVIWJVKSWGVIWIIVJGPUNUO + WHVKIGRHIGRZWJIWHVKHIGVIWFVLUPZUQWHUAUBUCVJIIFGAUAQZFTUBQZFTUCQZFTURWMW + NGRWOGRWMWNWOGRGRSBWGACDEWMWNWOFGMUSUTVIWFVLVBVIVRWGOUOZWPVCVIWKISZWGVI + HVJGRZVJSZWQDFIVJISZWRWKVJIVJIHGUHWTVDVEAWSDFUFZBAHVTGRZVTSZCFUFXAAXCCF + LUGXCWSCDFVTVJSZXBWRVTVJVTVJHGUHXDVDVEUJULUOOVFUOVGWLVGVH $. + $} + + ${ + grprinvd.x $e |- ( ( ph /\ ps ) -> X e. B ) $. + grprinvd.n $e |- ( ( ph /\ ps ) -> N e. B ) $. + grprinvd.e $e |- ( ( ph /\ ps ) -> ( N .+ X ) = O ) $. + $( Deduce right inverse from left inverse and left identity in an + associative structure (such as a group). (Contributed by NM, + 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) $) + grprinvd $p |- ( ( ph /\ ps ) -> ( X .+ N ) = O ) $= + ( co wcel vu vv vw wa cv caovclg adantlr caovcld wceq caovassg caovassd + 3expb w3a oveq1d oveq2 id eqeq12d wral ralrimiva cbvralv adantr rspcdva + sylib 3eqtr3d oveq2d eqtrd grprinvlem ) ABCDEFGIJHGSZKLMNOABUDZUAUBJHFF + FGAUAUEZFTZUBUEZFTZUDVJVLGSZFTBACDVJVLFFFGACUEZFTDUEZFTVOVPGSFTKULUFUGP + QUHZVIVHVHGSJHVHGSZGSVHVIUAUBUCJHVHFGAVKVMUCUEZFTUMVNVSGSVJVLVSGSGSUIBA + CDEVJVLVSFGNUJUGZPQVQUKVIVRHJGVIHJGSZHGSIHGSZVRHVIWAIHGRUNVIUAUBUCHJHFG + VTQPQUKVIIVPGSZVPUIZWBHUIDFHVPHUIZWCWBVPHVPHIGUOWEUPUQAWDDFURZBAIVOGSZV + OUIZCFURWFAWHCFMUSWHWDCDFVOVPUIZWGWCVOVPVOVPIGUOWIUPUQUTVCVAQVBVDVEVFVG + $. + $} + + $( Deduce right identity from left inverse and left identity in an + associative structure (such as a group). (Contributed by NM, + 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) $) + grpridd $p |- ( ( ph /\ x e. B ) -> ( x .+ O ) = x ) $= + ( vn vu vv cv wcel wa co wceq vw wrex oveq1 eqeq1d cbvrexv sylib caovassg + w3a adantlr simprl simprrl caovassd simprrr oveq1d oveq2d 3eqtr3d anassrs + grprinvd rexlimddv eqtr3d ) ABPZEQZRZGVAFSZVAGFSZVAVCMPZVAFSZGTZVDVETZMEV + CCPZVAFSZGTZCEUBVHMEUBLVLVHCMEVJVFTVKVGGVJVFVAFUCUDUEUFAVBVFEQZVHRZVIAVBV + NRZRZVAVFFSZVAFSVAVGFSVDVEVPNOUAVAVFVAEFANPZEQOPZEQUAPZEQUHVRVSFSVTFSVRVS + VTFSFSTVOABCDVRVSVTEFKUGUIAVBVNUJZAVBVMVHUKZWAULVPVQGVAFAVOBCDEFVFGVAHIJK + LWAWBAVBVMVHUMZURUNVPVGGVAFWCUOUPUQUSJUT $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -215614,6 +215678,28 @@ arbitrary magmas (then it should be called "iterated sum"). If the magma is SYGAUUNURXHXI $. $} + ${ + $d F x $. $d M x $. $d N x $. $d ph x $. + gsumsplit1r.b $e |- B = ( Base ` G ) $. + gsumsplit1r.p $e |- .+ = ( +g ` G ) $. + gsumsplit1r.g $e |- ( ph -> G e. V ) $. + gsumsplit1r.m $e |- ( ph -> M e. ZZ ) $. + gsumsplit1r.n $e |- ( ph -> N e. ( ZZ>= ` M ) ) $. + gsumsplit1r.f $e |- ( ph -> F : ( M ... ( N + 1 ) ) --> B ) $. + $( Splitting off the rightmost summand of a group sum. This corresponds to + the (inductive) definition of a (finite) product in [Lang] p. 4, first + formula. (Contributed by AV, 26-Dec-2023.) $) + gsumsplit1r $p |- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` ( M ... N ) ) ) + .+ ( F ` ( N + 1 ) ) ) ) $= + ( vx co cfv cfz wcel syl cgsu caddc cseq cres cuz peano2uz gsumval2 seqp1 + c1 wceq wss fzssp1 a1i fssresd uzidd cz eluzfz1 fvresd eqtrd cv wa fzp1ss + seq1 sselda seqfveq2 eqtr2d oveq1d 3eqtrd ) AEDUAPGUIUBPZCDFUCZQZGVJQZVID + QZCPZEDFGRPZUDZUAPZVMCPABCDEFVIHIJKAGFUEQZSZVIVRSMFGUFTNUGAVSVKVNUJMCDFGU + HTAVLVQVMCAVQGCVPFUCZQVLABCVPEFGHIJKMAFVIRPZBVODNVOWAUKAFGULUMUNUGACOVPDF + FGAFLUOAFVTQZFVPQZFDQAFUPSZWBWCUJLCVPFVCTAFVODAVSFVOSMFGUQTURUSMAOUTZFUIU + BPGRPZSVAWEVODAWFVOWEAWDWFVOUKLFGVBTVDURVEVFVGVH $. + $} + ${ gsumprval.b $e |- B = ( Base ` G ) $. gsumprval.p $e |- .+ = ( +g ` G ) $. @@ -215994,6 +216080,14 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is PMN $. $} + ${ + mndbn0.b $e |- B = ( Base ` G ) $. + $( The base set of a monoid is not empty. Statement in [Lang] p. 3. + (Contributed by AV, 29-Dec-2023.) $) + mndbn0 $p |- ( G e. Mnd -> B =/= (/) ) $= + ( cmnd wcel c0g cfv eqid mndidcl ne0d ) BDEABFGZABKCKHIJ $. + $} + ${ hashfinmndnn.1 $e |- B = ( Base ` G ) $. hashfinmndnn.2 $e |- ( ph -> G e. Mnd ) $. @@ -217304,10 +217398,48 @@ proposition to be be proved (the first four hypotheses tell its values ( cmnd wcel csubmnd cfv cword cgsu co submid gsumwsubmcl sylan ) BEFABGHF CAIFBCJKAFABDLABCMN $. - gsumccat.p $e |- .+ = ( +g ` G ) $. - $( Homomorphic property of composites. (Contributed by Stefan O'Rear, - 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) $) - gsumccat $p |- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> + gsumsgrpccat.p $e |- .+ = ( +g ` G ) $. + $( Homomorphic property of not empty composites of a group sum over a + semigroup. Formerly part of proof for ~ gsumccat . (Contributed by AV, + 26-Dec-2023.) $) + gsumsgrpccat $p |- ( ( G e. SGrp /\ ( W e. Word B /\ X e. Word B ) + /\ ( W =/= (/) /\ X =/= (/) ) ) + -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) $= + ( wcel wa cfv caddc co c1 cmin cc0 cseq wceq cn0 syl wf vx vy csgrp cword + vz c0 wne chash cconcat cgsu simp1 cmgm sgrpmgm mgmcl syl3an1 3expb sylan + w3a cv sgrpass cuz cn lennncl ad2ant2r 3adant1 nnzd uzidd nnm1nn0 uzaddcl + ad2ant2l syl2anc nncnd 1cnd addsubassd ax-1cn npcan sylancl 3eltr4d nn0uz + cc fveq2d syl6eleq cfz cfzo ccatcl 3ad2ant2 wrdf ccatlen oveq2d cz fzoval + zaddcld eqtrd feq2d mpbid seqsplit simpl2l simpl2r eleq2d biimpar syl3anc + ffvelrnda ccatval1 seqfveq addid2d eqtr4d seqeq1d addcomd addsubd fveq12d + oveq1d ccatval3 eqcomd seqshft2 oveq12d nnaddcld gsumval2 simp2l 3eqtr4d + simp2r ) CUCHZDAUDZHZEYBHZIZDUFUGZEUFUGZIZURZDUHJZEUHJZKLZMNLZBDEUILZOPZJ + ZYJMNLZBDOPJZYKMNLZBEOPJZBLZCYNUJLCDUJLZCEUJLZBLYIYPYQYOJZYMBYNYQMKLZPZJZ + BLUUAYIUAUBUEBAYNOYQYMYIYAUAUSZAHZUBUSZAHZIUUHUUJBLZAHZYAYEYHUKZYAUUIUUKU + UMYACULHUUIUUKUUMCUMACUUHUUJBFGUNUOUPUQYIYAUUIUUKUEUSZAHURUULUUOBLUUHUUJU + UOBLBLQUUNACUUHUUJBUUOFGUTUQYIYJYSKLZYJVAJZYMUUEVAJYIYJUUQHYSRHZUUPUUQHYI + YJYIYJYEYHYJVBHZYAYCYFUUSYDYGADVCVDVEZVFZVGYIYKVBHZUURYEYHUVBYAYDYGUVBYCY + FAEVCVJVEZYKVHSZYSYJYJVIVKYIYJYKMYIYJUUTVLZYIYKUVCVLZYIVMZVNYIUUEYJVAYIYJ + VTHMVTHUUEYJQUVEVOYJMVPVQZWAVRYIYQROVAJZYIUUSYQRHUUTYJVHSVSWBZYIOYMWCLZAU + UHYNYIOYNUHJZWDLZAYNTZUVKAYNTYIYNYBHZUVNYEYAUVOYHADEWEWFAYNWGSYIUVMUVKAYN + YIUVMOYLWDLZUVKYIUVLYLOWDYEYAUVLYLQYHADEWHWFWIYIYLWJHUVPUVKQYIYJYKUVAYIYK + UVCVFZWLOYLWKSWMWNWOZXBWPYIUUDYRUUGYTBYIBUAYNDOYQUVJYIUUHOYQWCLZHZIYCYDUU + HOYJWDLZHZUUHYNJUUHDJQYCYDYAYHUVTWQYCYDYAYHUVTWRYIUWBUVTYIUWAUVSUUHYIYJWJ + HUWAUVSQUVAOYJWKSZWSWTADEUUHXCXAXDYIUUGYSYJKLZBYNOYJKLZPZJYTYIYMUWDUUFUWF + YIUUEUWEBYNYIUUEYJUWEUVHYIYJUVEXEXFXGYIYMYKYJKLZMNLUWDYIYLUWGMNYIYJYKUVEU + VFXHXKYIYKYJMUVFUVEUVGXIWMXJYIBUAEYNYJOYSYIYSRUVIUVDVSWBZUVAYIUUHOYSWCLZH + ZIZUUHYJKLYNJZUUHEJZUWKYCYDUUHOYKWDLZHZUWLUWMQYCYDYAYHUWJWQYCYDYAYHUWJWRY + IUWOUWJYIUWNUWIUUHYIYKWJHUWNUWIQUVQOYKWKSZWSWTADEUUHXLXAXMXNXFXOWMYIABYNC + OYMUCFGUUNYIYMRUVIYIYLVBHYMRHYIYJYKUUTUVCXPYLVHSVSWBUVRXQYIUUBYRUUCYTBYIA + BDCOYQUCFGUUNUVJYIUWAADTZUVSADTYIYCUWQYAYCYDYHXRADWGSYIUWAUVSADUWCWNWOXQY + IABECOYSUCFGUUNUWHYIUWNAETZUWIAETYIYDUWRYAYCYDYHXTAEWGSYIUWNUWIAEUWPWNWOX + QXOXS $. + + $( Obsolete version of ~ gsumccat as of 13-Jan-2024. Homomorphic property + of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised + by Mario Carneiro, 1-Oct-2015.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + gsumccatOLD $p |- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) $= ( wcel co cgsu wceq c0 cfv oveq2d wa caddc c1 cc0 cn0 syl vx vy cword w3a vz cmnd cconcat c0g oveq1 oveq2 eqid gsum0 syl6eq oveq1d eqeq12d wne cmin @@ -217348,6 +217480,28 @@ proposition to be be proved (the first four hypotheses tell its values KYPYRYSUUOVOADYETNUUPYPUUCAHZUUSUUCKYPYRYSUUOUTYTUYNUUOYPYRUYNYSACDFYFYGY HABCUUCUUIFGUUMYKVQXPYIYTUUHUUDUUJYTUUGECJYSYPUUGEKYRAEYJYLNYPYRYSYPUUDAH UUJUUDKYPYRYSYMACEFYFABCUUDUUIFGUUMYNYOXPYI $. + $} + + ${ + gsumccat.b $e |- B = ( Base ` G ) $. + gsumccat.p $e |- .+ = ( +g ` G ) $. + $( Homomorphic property of composites. Second formula in [Lang] p. 4. + (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario + Carneiro, 1-Oct-2015.) (Proof shortened by AV, 26-Dec-2023.) $) + gsumccat $p |- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> + ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) $= + ( wcel cconcat co cgsu wceq c0 oveq2d oveq2 syl6eq eqeq12d wne ad2antrr + wa cmnd cword w3a c0g cfv oveq1 eqid gsum0 oveq1d mndsgrp 3ad2ant1 3simpc + csgrp simpr anim1i gsumsgrpccat syl3anc simpl2 ccatrid syl simpl1 gsumwcl + 3adant3 adantr mndrid syl2anc eqtr4d pm2.61ne ccatlid 3ad2ant3 3imp3i2an + simp1 mndlid ) CUAHZDAUBZHZEVOHZUCZCDEIJZKJZCDKJZCEKJZBJZLZCMEIJZKJZCUDUE + ZWBBJZLDMDMLZVTWFWCWHWIVSWECKDMEIUFNWIWAWGWBBWIWACMKJZWGDMCKOCWGWGUGZUHZP + UIQVRDMRZTZWDCDMIJZKJZWAWGBJZLEMEMLZVTWPWCWQWRVSWOCKEMDIONWRWBWGWABWRWBWJ + WGEMCKOWLPNQWNEMRZTCUMHZVPVQTZWMWSTWDVRWTWMWSVNVPWTVQCUJUKSVRXAWMWSVNVPVQ + ULSWNWMWSVRWMUNUOABCDEFGUPUQWNWPWAWQWNWODCKWNVPWODLVNVPVQWMURADUSUTNWNVNW + AAHZWQWALVNVPVQWMVAVRXBWMVNVPXBVQACDFVBVCVDABCWAWGFGWKVEVFVGVHVRWFWBWHVRW + EECKVQVNWEELVPAEVIVJNVNVPVQVNWBAHWHWBLVNVPVQVLACEFVBABCWBWGFGWKVMVKVGVH + $. $( Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) $) @@ -219932,6 +220086,36 @@ since the target of the homomorphism (operator ` O ` in our model) need VDSJKUFUJUQVGVCPURUQVGVFVCUQUTVAVFUQFOFUKULUMUQVBVCVEFUNUOTUPT $. $} + ${ + $d B i x $. $d F i $. $d N i x $. $d X i x $. + mulgnngsum.b $e |- B = ( Base ` G ) $. + mulgnngsum.t $e |- .x. = ( .g ` G ) $. + mulgnngsum.f $e |- F = ( x e. ( 1 ... N ) |-> X ) $. + $( Group multiple (exponentiation) operation at a positive integer + expressed by a group sum. (Contributed by AV, 28-Dec-2023.) $) + mulgnngsum $p |- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) ) $= + ( vi cn wcel wa cfv c1 cseq co adantr cv cplusg csn cxp cuz elnnuz biimpi + cgsu cfz cmpt wceq a1i eqidd simpr fvmptd elfznn fvconst2g syl2an seqfveq + weq eqtr4d cvv eqid elfvex eleq2s adantl fmptd gsumval2 mulgnn 3eqtr4rd + cbs ) FLMZGBMZNZFEUAOZDPQOFVNLGUBUCZPQZOEDUGRFGCRVMVNKDVOPFVKFPUDOMZVLVKV + QFUEUFSZVMKTZPFUHRZMZNZVSDOGVSVOOZWBAVSGGVTDBDAVTGUIUJWBJUKWBAKUSNGULVMWA + UMVMVLWAVKVLUMZSUNVMVLVSLMWCGUJWAWDVSFUOLGVSBUPUQUTURVMBVNDEPFVAHVNVBZVLE + VAMZVKWFGEVJOBGEVJVCHVDVEVRVMAVTGBDVMVLATVTMWDSJVFVGBVNVPCEFGHWEIVPVBVHVI + $. + + $( Group multiple (exponentiation) operation at a nonnegative integer + expressed by a group sum. This corresponds to the definition in [Lang] + p. 6, second formula. (Contributed by AV, 28-Dec-2023.) $) + mulgnn0gsum $p |- ( ( N e. NN0 /\ X e. B ) + -> ( N .x. X ) = ( G gsum F ) ) $= + ( wcel co cgsu wceq cc0 ex c0 c1 cfz syl6eq cn0 cn wo wi elnn0 mulgnngsum + wa c0g cfv oveq1 eqid mulg0 sylan9eq cmpt oveq2 fz10 eqidd mpteq12dv mpt0 + syl5eq adantr oveq2d gsum0 eqtr4d jaoi sylbi imp ) FUAKZGBKZFGCLZEDMLZNZV + HFUBKZFONZUCVIVLUDZFUEVMVOVNVMVIVLABCDEFGHIJUFPVNVIVLVNVIUGZVJEUHUIZVKVNV + IVJOGCLVQFOGCUJBCEGVQHVQUKZIULUMVPVKEQMLVQVPDQEMVNDQNVIVNDARFSLZGUNZQJVNV + TAQGUNQVNAVSGQGVNVSROSLQFORSUOUPTVNGUQURAGUSTUTVAVBEVQVRVCTVDPVEVFVG $. + $} + ${ mulg1.b $e |- B = ( Base ` G ) $. mulg1.m $e |- .x. = ( .g ` G ) $. @@ -221077,58 +221261,6 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario UMUNUKBCDEFACQNZULGRABDLPULHRAULSTIBUCUAUDUEABUIAUOBUINGBCEUFUBUGUH $. $} - ${ - $d m n s x A $. $d m n s u v x G $. $d x S $. $d x .x. $. $d m n x X $. - $d m n s u v F $. - cycsubg.x $e |- X = ( Base ` G ) $. - cycsubg.t $e |- .x. = ( .g ` G ) $. - cycsubg.f $e |- F = ( x e. ZZ |-> ( x .x. A ) ) $. - $( The set of integer powers of an element ` A ` of a group forms a - subgroup containing ` A ` , called the cyclic group generated by the - element ` A ` . (Contributed by Mario Carneiro, 13-Jan-2015.) $) - cycsubgcl $p |- ( ( G e. Grp /\ A e. X ) -> - ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) ) $= - ( vv wcel wa cfv cv co wral cz c1 wceq oveq1 vu vm cgrp crn csubg wss wne - vn cplusg cminusg mulgcl 3expa an32s fmptd frnd wfn ffnd fnfvelrn sylancl - c0 1z ne0d caddc df-3an eqid mulgdir sylan2br anass1rs zaddcl adantl ovex - w3a fvmpt syl ad2antrl ad2antll oveq12d 3eqtr4d syl2an eqeltrrd ralrimiva - anassrs wb oveq2 eleq1d ralrn adantr mpbird mulgneg znegcl fveq2d ralbidv - cneg jca fveq2 anbi12d issubg2 mpbir3and ax-mp mulg1 syl5eq ) EUCKZBFKZLZ - DUDZEUEMKZBXEKXDXFXEFUFZXEUTUGZUANZJNZEUIMZOZXEKZJXEPZXIEUJMZMZXEKZLZUAXE - PZXDQFDXDAQANZBCOZFDXBXTQKZXCYAFKZXBYBXCYCFCEXTBGHUKULUMIUNZUOXDXERDMZXDD - QUPZRQKZYEXEKXDQFDYDUQZVAQRDURUSZVBXDXSUBNZDMZXJXKOZXEKZJXEPZYKXOMZXEKZLZ - UBQPZXDYQUBQXDYJQKZLZYNYPYTYNYKUHNZDMZXKOZXEKZUHQPZYTUUDUHQXDYSUUAQKZUUDX - DYSUUFLZLZYJUUAVCOZDMZUUCXEUUHUUIBCOZYJBCOZUUABCOZXKOZUUJUUCXBUUGXCUUKUUN - SZUUGXCLXBYSUUFXCVLUUOYSUUFXCVDFXKCEYJUUABGHXKVEZVFVGVHUUHUUIQKZUUJUUKSUU - GUUQXDYJUUAVIZVJAUUIYAUUKQDXTUUIBCTIUUIBCVKVMVNUUHYKUULUUBUUMXKYSYKUULSZX - DUUFAYJYAUULQDXTYJBCTIYJBCVKVMZVOUUFUUBUUMSXDYSAUUAYAUUMQDXTUUABCTIUUABCV - KVMVPVQVRXDYFUUQUUJXEKUUGYHUURQUUIDURVSVTWBWAXDYNUUEWCZYSXDYFUVAYHYMUUDJU - HQDXJUUBSYLUUCXEXJUUBYKXKWDWEWFVNWGWHYTYJWMZDMZYOXEYTUVBBCOZUULXOMZUVCYOX - BYSXCUVDUVESZXBYSXCUVFFCEXOYJBGHXOVEZWIULUMYTUVBQKZUVCUVDSYSUVHXDYJWJZVJA - UVBYAUVDQDXTUVBBCTIUVBBCVKVMVNYTYKUULXOYSUUSXDUUTVJWKVRXDYFUVHUVCXEKYSYHU - VIQUVBDURVSVTWNWAXDYFXSYRWCYHXRYQUAUBQDXIYKSZXNYNXQYPUVJXMYMJXEUVJXLYLXEX - IYKXJXKTWEWLUVJXPYOXEXIYKXOWOWEWPWFVNWHXBXFXGXHXSVLWCXCUAJFXKXEEXOGUUPUVG - WQWGWRXDYEBXEXDYERBCOZBYGYEUVKSVAARYAUVKQDXTRBCTIRBCVKVMWSXCUVKBSXBFCEBGH - WTVJXAYIVTWN $. - - $( The cyclic subgroup generated by an element ` A ` is a subset of any - subgroup containing ` A ` . (Contributed by Mario Carneiro, - 13-Jan-2015.) $) - cycsubgss $p |- ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> ran F C_ S ) $= - ( csubg cfv wcel wa cz cv co subgmulgcl 3expa an32s fmptd frnd ) CFKLMZBC - MZNZOCEUEAOAPZBDQZCEUCUFOMZUDUGCMZUCUHUDUICDFUFBIRSTJUAUB $. - - $( The cyclic group generated by ` A ` is the smallest subgroup containing - ` A ` . (Contributed by Mario Carneiro, 13-Jan-2015.) $) - cycsubg $p |- ( ( G e. Grp /\ A e. X ) -> - ran F = |^| { s e. ( SubGrp ` G ) | A e. s } ) $= - ( cgrp wcel wa crn cv csubg cfv crab cint wss wi ssintab cycsubgss mpgbir - cab df-rab inteqi sseqtr4i a1i cycsubgcl eleq2 elrab sylibr intss1 eqssd - syl ) EKLBFLMZDNZBGOZLZGEPQZRZSZURVCTUQURUSVALUTMZGUEZSZVCURVFTVDURUSTUAG - VDGURUBABUSCDEFHIJUCUDVBVEUTGVAUFUGUHUIUQURVBLZVCURTUQURVALBURLZMVGABCDEF - HIJUJUTVHGURVAUSURBUKULUMURVBUNUPUO $. - $} - ${ $d x y A $. $d b g p s x y z G $. $d b g p s x y z .+ $. $d s x y z S $. $d y B $. $d b g p s x y z X $. @@ -221251,37 +221383,6 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario WMWOWLVQSVR $. $} - ${ - $d x y A $. $d x y G $. $d x .x. $. $d x y X $. $d y F $. $d y K $. - cycsubg2.x $e |- X = ( Base ` G ) $. - cycsubg2.t $e |- .x. = ( .g ` G ) $. - cycsubg2.f $e |- F = ( x e. ZZ |-> ( x .x. A ) ) $. - cycsubg2.k $e |- K = ( mrCls ` ( SubGrp ` G ) ) $. - $( The subgroup generated by an element is exhausted by its multiples. - (Contributed by Stefan O'Rear, 6-Sep-2015.) $) - cycsubg2 $p |- ( ( G e. Grp /\ A e. X ) -> ( K ` { A } ) = ran F ) $= - ( vy cgrp wcel wa csn wss cfv crab cint cv csubg crn snssg bicomd rabbidv - wb adantl inteqd cmre subgacs acsmred snssi mrcval syl2an cycsubg 3eqtr4d - wceq ) EMNZBGNZOZBPZLUAZQZLEUBRZSZTZBVCNZLVESZTVBFRZDUCVAVFVIVAVDVHLVEUTV - DVHUGUSUTVHVDBVCGUDUEUHUFUIUSVEGUJRNVBGQVJVGURUTUSVEGGEHUKULBGUMVEVBFGLKU - NUOABCDEGLHIJUPUQ $. - $} - - ${ - cycsubg2cl.x $e |- X = ( Base ` G ) $. - cycsubg2cl.t $e |- .x. = ( .g ` G ) $. - cycsubg2cl.k $e |- K = ( mrCls ` ( SubGrp ` G ) ) $. - $( Any multiple of an element is contained in the generated cyclic - subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) $) - cycsubg2cl $p |- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> - ( N .x. A ) e. ( K ` { A } ) ) $= - ( cgrp wcel cz w3a csn cfv csubg co cmre wss subgacs 3ad2ant1 simp2 snssd - acsmred mrccl syl2anc simp3 mrcssidd wb snssg 3ad2ant2 subgmulgcl syl3anc - mpbird ) CJKZAFKZELKZMZANZDOZCPOZKZUQAUTKZEABQUTKURVAFROKZUSFSVBUOUPVDUQU - OVAFFCGTUDUAZURAFUOUPUQUBUCZVAUSDFIUEUFUOUPUQUGURVCUSUTSZURVAUSDFVEIVFUHU - PUOVCVGUIUQAUTFUJUKUNUTBCEAHULUM $. - $} - ${ $d x z A $. $d z B $. $d u w x y z G $. $d u w z N $. $d u w x y z S $. $d u w x y z .+ $. $d w z H $. $d u w x y z X $. @@ -221748,6 +221849,182 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Cyclic monoids and groups +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + + This section contains some preliminary results about cyclic monoids and + groups before the class ` CycGrp ` of cyclic groups (see ~ df-cyg ) is + defined in the cointext of abelian groups. + +$) + + ${ + $d A x $. $d F i $. $d X i $. $d i x $. $d .x. x $. + cycsubm.b $e |- B = ( Base ` G ) $. + cycsubm.t $e |- .x. = ( .g ` G ) $. + cycsubm.f $e |- F = ( x e. NN0 |-> ( x .x. A ) ) $. + cycsubm.c $e |- C = ran F $. + $( Characterization of an element of the set of nonnegative integer powers + of an element ` A ` . Although this theorem holds for any class ` G ` , + the definition of ` F ` is only meaningful if ` G ` is a monoid or at + least a unital magma. (Contributed by AV, 28-Dec-2023.) $) + cycsubmel $p |- ( X e. C <-> E. i e. NN0 X = ( i .x. A ) ) $= + ( wcel cv wceq cn0 wrex co ovex crn cfv eleq2i wfn wb fvelrnb ax-mp oveq1 + fnmpti fvmpt eqeq1d eqcom syl6bb rexbiia 3bitri ) IDNIGUAZNZFOZGUBZIPZFQR + ZIURBESZPZFQRDUPIMUCGQUDUQVAUEAQAOZBESZGVDBETLUIFQIGUFUGUTVCFQURQNZUTVBIP + VCVFUSVBIAURVEVBQGVDURBEUHLURBETUJUKVBIULUMUNUO $. + + $d A i $. $d B i $. $d .x. i $. + $( The set of nonnegative integer powers of an element ` A ` contains + ` A ` . Although this theorem holds for any class ` G ` , the + definition of ` F ` is only meaningful if ` G ` is a monoid or at least + a unital magma. (Contributed by AV, 28-Dec-2023.) $) + cycsubmcl $p |- ( A e. B -> A e. C ) $= + ( vi wcel cv co wceq cn0 wrex c1 1nn0 wb oveq1 eqeq2d adantl mulg1 eqcomd + a1i rspcedvd cycsubmel sylibr ) BCMZBLNZBEOZPZLQRBDMUKUNBSBEOZPZLSQSQMUKT + UGULSPZUNUPUAUKUQUMUOBULSBEUBUCUDUKUOBCEGBHIUEUFUHABCDELFGBHIJKUIUJ $. + + $d A a b j k $. $d B a b j k x $. $d C a b $. $d F j k $. + $d G a b i j k x $. $d .x. j k $. + $( The set of nonnegative integer powers of an element ` A ` of a monoid + forms a submonoid containing ` A ` (see ~ cycsubmcl ), called the cyclic + monoid generated by the element ` A ` . This corresponds to the + statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.) $) + cycsubm $p |- ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) ) $= + ( va vi wcel wa cv co cn0 wceq cc0 vb vj vk cmnd csubmnd cfv wss c0g wral + cplusg crn mulgnn0cl 3expa an32s fmptd frnd eqsstrid wrex 0nn0 a1i eqeq2d + wb oveq1 adantl mulg0 eqcomd rspcedvd cycsubmel sylibr caddc simplr simpr + eqid wi nn0addcld adantr oveq12 ancoms simplll simpllr syl13anc sylan9eqr + mulgnn0dir exp32 rexlimdva com23 impd anbi12i 3imtr4g ralrimivv mpbir3and + w3a issubm ) GUDNZBCNZOZDGUEUFNZDCUGZGUHUFZDNZLPZUAPZGUJUFZQZDNZUADUILDUI + ZWPDFUKCKWPRCFWPARAPZBEQZCFWNXGRNZWOXHCNZWNXIWOXJCEGXGBHIULUMUNJUOUPUQWPW + SMPZBEQZSZMRURWTWPXMWSTBEQZSZMTRTRNWPUSUTXKTSZXMXOVBWPXPXLXNWSXKTBEVCVAVD + WPXNWSWOXNWSSWNCEGBWSHWSVMZIVEVDVFVGABCDEMFGWSHIJKVHVIWPXELUADDWPXAXLSZMR + URZXBUBPZBEQZSZUBRURZOXDUCPZBEQZSZUCRURZXADNZXBDNZOXEWPXSYCYGWPXRYCYGVNMR + WPXKRNZOZYCXRYGYKYBXRYGVNUBRYKXTRNZOZYBXRYGYMYBXROZOZYFXDXKXTVJQZBEQZSZUC + YPRYMYPRNYNYMXKXTWPYJYLVKZYKYLVLZVOVPYDYPSZYFYRVBYOUUAYEYQXDYDYPBEVCVAVDY + NYMXDXLYAXCQZYQXRYBXDUUBSXAXLXBYAXCVQVRYMYQUUBYMWNYJYLWOYQUUBSWNWOYJYLVSY + SYTWNWOYJYLVTCXCEGXKXTBHIXCVMZWCWAVFWBVGWDWEWFWEWGYHXSYIYCABCDEMFGXAHIJKV + HABCDEUBFGXBHIJKVHWHABCDEUCFGXDHIJKVHWIWJWNWQWRWTXFWLVBWOLUACXCDGWSHXQUUC + WMVPWK $. + $} + + ${ + $d ph n $. $d A n $. + cycsubggend.1 $e |- B = ( Base ` G ) $. + cycsubggend.2 $e |- .x. = ( .g ` G ) $. + cycsubggend.3 $e |- F = ( n e. ZZ |-> ( n .x. A ) ) $. + cycsubggend.4 $e |- ( ph -> A e. B ) $. + $( The cyclic subgroup generated by ` A ` includes its generator. Although + this theorem holds for any class ` G ` , the definition of ` F ` is only + meaningful if ` G ` is a group. (Contributed by Rohan Ridenour, + 3-Aug-2023.) $) + cycsubggend $p |- ( ph -> A e. ran F ) $= + ( cz cv co c1 1zzd wceq wa simpr oveq1d adantr mulg1 syl eqtr2d elrnmptdv + wcel ) AELEMZBDNZOBFCJAPKAUGOQZRZUHOBDNZBUJUGOBDAUISTUJBCUFZUKBQAULUIKUAC + DGBHIUBUCUDUE $. + $} + + ${ + $d m n s x A $. $d m n s u v x G $. $d x S $. $d x .x. $. $d m n x X $. + $d m n s u v F $. + cycsubg.x $e |- X = ( Base ` G ) $. + cycsubg.t $e |- .x. = ( .g ` G ) $. + cycsubg.f $e |- F = ( x e. ZZ |-> ( x .x. A ) ) $. + $( The set of integer powers of an element ` A ` of a group forms a + subgroup containing ` A ` , called the cyclic group generated by the + element ` A ` . (Contributed by Mario Carneiro, 13-Jan-2015.) $) + cycsubgcl $p |- ( ( G e. Grp /\ A e. X ) -> + ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) ) $= + ( vv wcel wa cfv cv co wral cz c1 wceq oveq1 vu vm cgrp crn csubg wss wne + vn cplusg cminusg mulgcl 3expa an32s fmptd frnd wfn ffnd fnfvelrn sylancl + c0 1z ne0d caddc df-3an eqid mulgdir sylan2br anass1rs zaddcl adantl ovex + w3a fvmpt syl ad2antrl ad2antll oveq12d 3eqtr4d syl2an eqeltrrd ralrimiva + anassrs wb oveq2 eleq1d ralrn adantr mpbird mulgneg znegcl fveq2d ralbidv + cneg jca fveq2 anbi12d issubg2 mpbir3and ax-mp mulg1 syl5eq ) EUCKZBFKZLZ + DUDZEUEMKZBXEKXDXFXEFUFZXEUTUGZUANZJNZEUIMZOZXEKZJXEPZXIEUJMZMZXEKZLZUAXE + PZXDQFDXDAQANZBCOZFDXBXTQKZXCYAFKZXBYBXCYCFCEXTBGHUKULUMIUNZUOXDXERDMZXDD + QUPZRQKZYEXEKXDQFDYDUQZVAQRDURUSZVBXDXSUBNZDMZXJXKOZXEKZJXEPZYKXOMZXEKZLZ + UBQPZXDYQUBQXDYJQKZLZYNYPYTYNYKUHNZDMZXKOZXEKZUHQPZYTUUDUHQXDYSUUAQKZUUDX + DYSUUFLZLZYJUUAVCOZDMZUUCXEUUHUUIBCOZYJBCOZUUABCOZXKOZUUJUUCXBUUGXCUUKUUN + SZUUGXCLXBYSUUFXCVLUUOYSUUFXCVDFXKCEYJUUABGHXKVEZVFVGVHUUHUUIQKZUUJUUKSUU + GUUQXDYJUUAVIZVJAUUIYAUUKQDXTUUIBCTIUUIBCVKVMVNUUHYKUULUUBUUMXKYSYKUULSZX + DUUFAYJYAUULQDXTYJBCTIYJBCVKVMZVOUUFUUBUUMSXDYSAUUAYAUUMQDXTUUABCTIUUABCV + KVMVPVQVRXDYFUUQUUJXEKUUGYHUURQUUIDURVSVTWBWAXDYNUUEWCZYSXDYFUVAYHYMUUDJU + HQDXJUUBSYLUUCXEXJUUBYKXKWDWEWFVNWGWHYTYJWMZDMZYOXEYTUVBBCOZUULXOMZUVCYOX + BYSXCUVDUVESZXBYSXCUVFFCEXOYJBGHXOVEZWIULUMYTUVBQKZUVCUVDSYSUVHXDYJWJZVJA + UVBYAUVDQDXTUVBBCTIUVBBCVKVMVNYTYKUULXOYSUUSXDUUTVJWKVRXDYFUVHUVCXEKYSYHU + VIQUVBDURVSVTWNWAXDYFXSYRWCYHXRYQUAUBQDXIYKSZXNYNXQYPUVJXMYMJXEUVJXLYLXEX + IYKXJXKTWEWLUVJXPYOXEXIYKXOWOWEWPWFVNWHXBXFXGXHXSVLWCXCUAJFXKXEEXOGUUPUVG + WQWGWRXDYEBXEXDYERBCOZBYGYEUVKSVAARYAUVKQDXTRBCTIRBCVKVMWSXCUVKBSXBFCEBGH + WTVJXAYIVTWN $. + + $( The cyclic subgroup generated by an element ` A ` is a subset of any + subgroup containing ` A ` . (Contributed by Mario Carneiro, + 13-Jan-2015.) $) + cycsubgss $p |- ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> ran F C_ S ) $= + ( csubg cfv wcel wa cz cv co subgmulgcl 3expa an32s fmptd frnd ) CFKLMZBC + MZNZOCEUEAOAPZBDQZCEUCUFOMZUDUGCMZUCUHUDUICDFUFBIRSTJUAUB $. + + $( The cyclic group generated by ` A ` is the smallest subgroup containing + ` A ` . (Contributed by Mario Carneiro, 13-Jan-2015.) $) + cycsubg $p |- ( ( G e. Grp /\ A e. X ) -> + ran F = |^| { s e. ( SubGrp ` G ) | A e. s } ) $= + ( cgrp wcel wa crn cv csubg cfv crab cint wss wi ssintab cycsubgss mpgbir + cab df-rab inteqi sseqtr4i a1i cycsubgcl eleq2 elrab sylibr intss1 eqssd + syl ) EKLBFLMZDNZBGOZLZGEPQZRZSZURVCTUQURUSVALUTMZGUEZSZVCURVFTVDURUSTUAG + VDGURUBABUSCDEFHIJUCUDVBVEUTGVAUFUGUHUIUQURVBLZVCURTUQURVALBURLZMVGABCDEF + HIJUJUTVHGURVAUSURBUKULUMURVBUNUPUO $. + $} + + ${ + $d G n $. $d .x. n $. $d B n $. $d A n $. + cycsubgcld.1 $e |- B = ( Base ` G ) $. + cycsubgcld.2 $e |- .x. = ( .g ` G ) $. + cycsubgcld.3 $e |- F = ( n e. ZZ |-> ( n .x. A ) ) $. + cycsubgcld.4 $e |- ( ph -> G e. Grp ) $. + cycsubgcld.5 $e |- ( ph -> A e. B ) $. + $( The cyclic subgroup generated by ` A ` is a subgroup. Deduction related + to ~ cycsubgcl . (Contributed by Rohan Ridenour, 3-Aug-2023.) $) + cycsubgcld $p |- ( ph -> ran F e. ( SubGrp ` G ) ) $= + ( crn csubg cfv wcel cgrp wa cycsubgcl syl2anc simpld ) AFMZGNOPZBUBPZAGQ + PBCPUCUDRKLEBDFGCHIJSTUA $. + $} + + ${ + $d x y A $. $d x y G $. $d x .x. $. $d x y X $. $d y F $. $d y K $. + cycsubg2.x $e |- X = ( Base ` G ) $. + cycsubg2.t $e |- .x. = ( .g ` G ) $. + cycsubg2.f $e |- F = ( x e. ZZ |-> ( x .x. A ) ) $. + cycsubg2.k $e |- K = ( mrCls ` ( SubGrp ` G ) ) $. + $( The subgroup generated by an element is exhausted by its multiples. + (Contributed by Stefan O'Rear, 6-Sep-2015.) $) + cycsubg2 $p |- ( ( G e. Grp /\ A e. X ) -> ( K ` { A } ) = ran F ) $= + ( vy cgrp wcel wa csn wss cfv crab cint cv csubg crn snssg bicomd rabbidv + wb adantl inteqd cmre subgacs acsmred snssi mrcval syl2an cycsubg 3eqtr4d + wceq ) EMNZBGNZOZBPZLUAZQZLEUBRZSZTZBVCNZLVESZTVBFRZDUCVAVFVIVAVDVHLVEUTV + DVHUGUSUTVHVDBVCGUDUEUHUFUIUSVEGUJRNVBGQVJVGURUTUSVEGGEHUKULBGUMVEVBFGLKU + NUOABCDEGLHIJUPUQ $. + $} + + ${ + cycsubg2cl.x $e |- X = ( Base ` G ) $. + cycsubg2cl.t $e |- .x. = ( .g ` G ) $. + cycsubg2cl.k $e |- K = ( mrCls ` ( SubGrp ` G ) ) $. + $( Any multiple of an element is contained in the generated cyclic + subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) $) + cycsubg2cl $p |- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> + ( N .x. A ) e. ( K ` { A } ) ) $= + ( cgrp wcel cz w3a csn cfv csubg co cmre wss subgacs 3ad2ant1 simp2 snssd + acsmred mrccl syl2anc simp3 mrcssidd wb snssg 3ad2ant2 subgmulgcl syl3anc + mpbird ) CJKZAFKZELKZMZANZDOZCPOZKZUQAUTKZEABQUTKURVAFROKZUSFSVBUOUPVDUQU + OVAFFCGTUDUAZURAFUOUPUQUBUCZVAUSDFIUEUFUOUPUQUGURVCUSUTSZURVAUSDFVEIVFUHU + PUOVCVGUIUQAUTFUJUKUNUTBCEAHULUM $. + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Elementary theory of group homomorphisms @@ -228780,10 +229057,25 @@ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) ) $= VAUTWDJIVJACBDVGWCFSUPTUQUR $. $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Direct products (extension) +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + ${ - $d a c x y z .(+) $. $d a b c x y z G $. $d a b c x y z R $. - $d a b c x y z T $. $d a b c x y z U $. + $d G x y $. $d U x y $. lsmub1.p $e |- .(+) = ( LSSum ` G ) $. + $( The direct product is idempotent for submonoids. (Contributed by AV, + 27-Dec-2023.) $) + smndlsmidm $p |- ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = U ) $= + ( vx vy csubmnd cfv wcel co cv cplusg cmpo crn cdm cbs wss wceq eqid wral + elfvdm submss lsmvalx syl3anc cxp submcl 3expb ralrimivva fmpo sylib frnd + wf eqsstrd lsmub1x mpancom eqssd ) BCGHIZBBAJZBUQUREFBBEKZFKZCLHZJZMZNZBU + QCGOZIBCPHZQZVGURVDRBCGUAVFBCVFSZUBZVIEFVFVAABBCVEVHVASZDUCUDUQBBUEZBVCUQ + VBBIZFBTEBTVKBVCULUQVLEFBBUQUSBIUTBIVLVABCUSUTVJUFUGUHEFBBVBBVCVCSUIUJUKU + MVGUQBURQVIVFABBCVHDUNUOUP $. + $( Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) $) lsmub1 $p |- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> @@ -228832,8 +229124,17 @@ U C_ ( T .(+) U ) ) $= FNVDGUDUEUQUKULUOUSUTLUKULUPUFUKULUPUGVEACDEFGUHUIT $. $( Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised - by Mario Carneiro, 21-Jun-2014.) $) + by Mario Carneiro, 21-Jun-2014.) (Proof shortened by AV, + 27-Dec-2023.) $) lsmidm $p |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) $= + ( csubg cfv wcel csubmnd co wceq subgsubm smndlsmidm syl ) BCEFGBCHFGBBAI + BJBCKABCDLM $. + + $( Obsolete proof of ~ lsmidm as of 13-Jan-2023. Subgroup sum is + idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario + Carneiro, 21-Jun-2014.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + lsmidmOLD $p |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) $= ( vx vy csubg cfv wcel co cv cplusg cmpo crn wceq eqid lsmval anidms wral cbs cxp subgcl 3expb ralrimivva fmpo sylib frnd eqsstrd wss lsmub1 eqssd wf ) BCGHIZBBAJZBUMUNEFBBEKZFKZCLHZJZMZNZBUMUNUTOEFCTHZUQABBCVAPUQPZDQRUM @@ -228881,6 +229182,8 @@ U C_ ( T .(+) U ) ) $= ( csubg cfv wcel wa wss wceq lsmss2 3expia lsmub2 sseq2 syl5ibcom impbid co ) BDFGZHZCSHZIZCBJZBCARZBKZTUAUCUEABCDELMUBCUDJUEUCABCDENUDBCOPQ $. + $d G a b c z $. $d R a b c x y z $. $d T a b c x y z $. $d U a b c z $. + $d .(+) a c x y z $. $( Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) $) lsmass $p |- ( ( R e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ @@ -228907,6 +229210,16 @@ U C_ ( T .(+) U ) ) $= CDEYEFWBWCIJYDXAABWPEVDWRYEYFFWDWCWEWF $. $} + ${ + mndlsmidm.p $e |- .(+) = ( LSSum ` G ) $. + mndlsmidm.b $e |- B = ( Base ` G ) $. + $( Subgroup sum is idempotent for monoids. This corresponds to the + observation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) $) + mndlsmidm $p |- ( G e. Mnd -> ( B .(+) B ) = B ) $= + ( cmnd wcel csubmnd cfv co wceq submid smndlsmidm syl ) CFGACHIGAABJAKACE + LBACDMN $. + $} + ${ lsm01.z $e |- .0. = ( 0g ` G ) $. lsm01.p $e |- .(+) = ( LSSum ` G ) $. @@ -231600,6 +231913,28 @@ an extension of the previous (inserting an element and its inverse at PEGCPFCPQADROUCJDSTKLMBCDEFGHIUAUB $. $} + ${ + $d A v w $. $d B v w $. $d .0. v w $. $d .+ v w $. $d ph v w $. + invmod.b $e |- B = ( Base ` G ) $. + invmod.0 $e |- .0. = ( 0g ` G ) $. + invmod.p $e |- .+ = ( +g ` G ) $. + invmod.m $e |- ( ph -> G e. CMnd ) $. + invmod.a $e |- ( ph -> A e. B ) $. + $( Uniqueness of an inverse element in a commutative monoid, if it exists. + Corresponds to ~ caovmo . (Contributed by AV, 31-Dec-2023.) $) + invmod $p |- ( ph -> E* w e. B ( A .+ w ) = .0. ) $= + ( vv cv co wceq wa wcel adantr adantl wi wral wrmo cmnd ccmn cmnmnd simpl + weq syl mndrid syl2an eqcomd oveq2 eqcoms simpr w3a mndass cmncom syl3anc + syl13anc sylan9eq oveq1d mndlid 3eqtrd ex ralrimivva eqeq1d rmo4 sylibr ) + ACBNZEOZGPZCMNZEOZGPZQZBMUHZUAZMDUBBDUBVLBDUCAVRBMDDAVJDRZVMDRZQZQZVPVQWB + VPQZVJVJGEOZVJVNEOZVMWBVJWDPVPWBWDVJAFUDRZVSWDVJPWAAFUERZWFKFUFUIZVSVTUGZ + DEFVJGHJIUJUKULSVPWDWEPZWBVOWJVLWJGVNGVNVJEUMUNTTWCWEVJCEOZVMEOZGVMEOZVMW + BWEWLPZVPWBWFVSCDRZVTWNAWFWAWHSWAVSAWITZAWOWALSZWAVTAVSVTUOZTWFVSWOVTUPQW + LWEDEFVJCVMHJUQULUTSWCWKGVMEWBVPWKVKGWBWGVSWOWKVKPAWGWAKSWPWQDEFVJCHJURUS + VLVOUGVAVBWBWMVMPZVPAWFVTWSWAWHWRDEFVMGHJIVCUKSVDVDVEVFVLVOBMDVQVKVNGVJVM + CEUMVGVHVI $. + $} + ${ ablinvadd.b $e |- B = ( Base ` G ) $. ablinvadd.p $e |- .+ = ( +g ` G ) $. @@ -233533,6 +233868,20 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements QRZJKUGSZAFUATFUBTLFUCUDMNABCEFUGJUHLNUEOPUF $. $} + ${ + gsumreidx.b $e |- B = ( Base ` G ) $. + gsumreidx.z $e |- .0. = ( 0g ` G ) $. + gsumreidx.g $e |- ( ph -> G e. CMnd ) $. + gsumreidx.f $e |- ( ph -> F : ( M ... N ) --> B ) $. + gsumreidx.h $e |- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) ) $. + $( Re-index a finite group sum using a bijection. Corresponds to the first + equation in [Lang] p. 5 with ` M = 1 ` . (Contributed by AV, + 26-Dec-2023.) $) + gsumreidx $p |- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) $= + ( cfz co cvv ovexd fzfid wcel c0g fvexi a1i fdmfifsupp gsumf1o ) AFGNOZBU + ECDEPHIJKAFGNQLAUEBCPHLAFGRHPSAHDTJUAUBUCMUD $. + $} + ${ gsumzsubmcl.0 $e |- .0. = ( 0g ` G ) $. gsumzsubmcl.z $e |- Z = ( Cntz ` G ) $. @@ -234981,6 +235330,72 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements AZQUCRSTQUIGUBDUAZUDUJUIUDUEAUIUJUFUGUH $. $} + ${ + $d j k A $. $d j k B $. $d j k C $. $d j k G $. $d j k U $. $d j V $. + $d j k .0. $. $d j k ph $. $d k W $. + gsumcom3.b $e |- B = ( Base ` G ) $. + gsumcom3.z $e |- .0. = ( 0g ` G ) $. + gsumcom3.g $e |- ( ph -> G e. CMnd ) $. + gsumcom3.a $e |- ( ph -> A e. V ) $. + gsumcom3.r $e |- ( ph -> C e. W ) $. + gsumcom3.f $e |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B ) $. + gsumcom3.u $e |- ( ph -> U e. Fin ) $. + gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) + -> X = .0. ) $. + $( A commutative law for finitely supported iterated sums. (Contributed by + Stefan O'Rear, 2-Nov-2015.) $) + gsumcom3 $p |- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> + X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) ) $= + ( cmpo cgsu co cmpt gsumcom wcel cv adantr gsum2d2 ccnv ancom2s cfn cnvfi + syl wa wbr wn wceq ancom vex brcnv notbii anbi12i sylan2b 3eqtr3d ) AHFGB + DKUAUBUCHGFDBKUAUBUCHFBHGDKUDUBUCUDUBUCHGDHFBKUDUBUCUDUBUCABCDEFGHIJKLMNO + PQRSTUEABCDEFGHIJKLMNOPADJUFFUGZBUFZQUHRSTUIADCBEUJZGFHJIKLMNOQABIUFGUGZD + UFZPUHAVGVJKCUFRUKAEULUFVHULUFSEUMUNVJVGUOZVIVFVHUPZUQZUOAVGVJUOZVFVIEUPZ + UQZUOKLURVKVNVMVPVJVGUSVLVOVIVFEGUTFUTVAVBVCTVDUIVE $. + $} + + ${ + $d j k A $. $d j k B $. $d j k C $. $d j k G $. $d j k ph $. + gsumcom3fi.b $e |- B = ( Base ` G ) $. + gsumcom3fi.g $e |- ( ph -> G e. CMnd ) $. + gsumcom3fi.a $e |- ( ph -> A e. Fin ) $. + gsumcom3fi.r $e |- ( ph -> C e. Fin ) $. + gsumcom3fi.f $e |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B ) $. + $( A commutative law for finite iterated sums. (Contributed by Stefan + O'Rear, 5-Sep-2015.) $) + gsumcom3fi $p |- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> + X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) ) $= + ( cxp cfn c0g cfv wcel cv wa eqid xpfi syl2anc wbr wn wceq biimpri adantl + brxp pm2.24d impr gsumcom3 ) ABCDBDNZEFGOOHGPQZIUNUAJKLMABORDORUMORKLBDUB + UCAESZBRFSZDRTZUOUPUMUDZUEHUNUFZAUQTURUSUQURAURUQUOUPBDUIUGUHUJUKUL $. + $} + + ${ + $d A j k $. $d B j k $. $d C j k $. $d G j k $. $d F j k $. $d V j $. + $d W k $. $d .0. j k $. $d ph j k $. + gsumxp2.b $e |- B = ( Base ` G ) $. + gsumxp2.z $e |- .0. = ( 0g ` G ) $. + gsumxp2.g $e |- ( ph -> G e. CMnd ) $. + gsumxp2.a $e |- ( ph -> A e. V ) $. + gsumxp2.r $e |- ( ph -> C e. W ) $. + gsumxp2.f $e |- ( ph -> F : ( A X. C ) --> B ) $. + gsumxp2.w $e |- ( ph -> F finSupp .0. ) $. + $( Write a group sum over a cartesian product as a double sum in two ways. + This corresponds to the first equation in [Lang] p. 6. (Contributed by + AV, 27-Dec-2023.) $) + gsumxp2 $p |- ( ph + -> ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> ( j F k ) ) ) ) ) + = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) ) $= + ( co wcel cv cmpt cgsu csupp fovrnda fsuppimpd wa wbr wn wceq cop cfv cxp + simpl opelxpi ad2antlr simpr eldifd cvv ssidd xpexd c0g fvexi a1i suppssr + cdif syl2an2r ex df-br notbii df-ov eqeq1i 3imtr4g impr gsumcom3 eqcomd ) + AHEBHFDEUAZFUAZGSZUBUCSUBUCSHFDHEBVSUBUCSUBUCSABCDGKUDSZEFHIJVSKLMNOPAVQV + RCBDGQUEAGKRUFAVQBTVRDTUGZVQVRVTUHZUIZVSKUJZAWAUGZVQVRUKZVTTZUIZWFGULZKUJ + ZWCWDWEWHWJWEAWHWFBDUMZVTVFTWJAWAUNWEWHUGWFWKVTWAWFWKTAWHVQVRBDUOUPWEWHUQ + URAWKCUSGUSVTWFKQAVTUTABDIJOPVAKUSTAKHVBMVCVDVEVGVHWBWGVQVRVTVIVJVSWIKVQV + RGVKVLVMVNVOVP $. + $} + ${ $d a x y I $. $d a x y J $. $d a R $. $d a U $. $d a x y Y $. $d a x y ph $. @@ -238158,10 +238573,17 @@ factorization into prime power factors (even if the exponents are ACDIUAJKLMNUUBUUC $. $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Simple groups =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Definition and basic properties +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) $c SimpGrp $. @@ -238314,42 +238736,13 @@ elements and the subgroup containing only the identity ( ~ simpgnsgbid ). LUNUPURRAUOURUEUFUQUMBUGUHUIUJ $. $} + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Classification of abelian simple groups -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d ph n $. $d A n $. - cycsubggend.1 $e |- B = ( Base ` G ) $. - cycsubggend.2 $e |- .x. = ( .g ` G ) $. - cycsubggend.3 $e |- F = ( n e. ZZ |-> ( n .x. A ) ) $. - cycsubggend.4 $e |- ( ph -> A e. B ) $. - $( The cyclic subgroup generated by ` A ` includes its generator. Although - this theorem holds for any class ` G ` , the definition of ` F ` is only - meaningful if ` G ` is a group. (Contributed by Rohan Ridenour, - 3-Aug-2023.) $) - cycsubggend $p |- ( ph -> A e. ran F ) $= - ( cz cv co c1 1zzd wceq wa simpr oveq1d adantr mulg1 syl eqtr2d elrnmptdv - wcel ) AELEMZBDNZOBFCJAPKAUGOQZRZUHOBDNZBUJUGOBDAUISTUJBCUFZUKBQAULUIKUAC - DGBHIUBUCUDUE $. - $} - - ${ - $d G n $. $d .x. n $. $d B n $. $d A n $. - cycsubgcld.1 $e |- B = ( Base ` G ) $. - cycsubgcld.2 $e |- .x. = ( .g ` G ) $. - cycsubgcld.3 $e |- F = ( n e. ZZ |-> ( n .x. A ) ) $. - cycsubgcld.4 $e |- ( ph -> G e. Grp ) $. - cycsubgcld.5 $e |- ( ph -> A e. B ) $. - $( The cyclic subgroup generated by ` A ` is a subgroup. Deduction related - to ~ cycsubgcl . (Contributed by Rohan Ridenour, 3-Aug-2023.) $) - cycsubgcld $p |- ( ph -> ran F e. ( SubGrp ` G ) ) $= - ( crn csubg cfv wcel cgrp wa cycsubgcl syl2anc simpld ) AFMZGNOPZBUBPZAGQ - PBCPUCUDRKLEBDFGCHIJSTUA $. - $} - ${ ablsimpnosubgd.1 $e |- B = ( Base ` G ) $. ablsimpnosubgd.2 $e |- .0. = ( 0g ` G ) $. @@ -267999,46 +268392,6 @@ as element of (the base set of) ` ( ( 1 ... n ) Mat R ) `. $. $} - ${ - $d j k A $. $d j k B $. $d j k C $. $d j k G $. $d j k U $. $d j V $. - $d j k .0. $. $d j k ph $. $d k W $. - gsumcom3.b $e |- B = ( Base ` G ) $. - gsumcom3.z $e |- .0. = ( 0g ` G ) $. - gsumcom3.g $e |- ( ph -> G e. CMnd ) $. - gsumcom3.a $e |- ( ph -> A e. V ) $. - gsumcom3.r $e |- ( ph -> C e. W ) $. - gsumcom3.f $e |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B ) $. - gsumcom3.u $e |- ( ph -> U e. Fin ) $. - gsumcom3.n $e |- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) - -> X = .0. ) $. - $( A commutative law for finitely supported iterated sums. (Contributed by - Stefan O'Rear, 2-Nov-2015.) $) - gsumcom3 $p |- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> - X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) ) $= - ( cmpo cgsu co cmpt gsumcom wcel cv adantr gsum2d2 ccnv ancom2s cfn cnvfi - syl wa wbr wn wceq ancom vex brcnv notbii anbi12i sylan2b 3eqtr3d ) AHFGB - DKUAUBUCHGFDBKUAUBUCHFBHGDKUDUBUCUDUBUCHGDHFBKUDUBUCUDUBUCABCDEFGHIJKLMNO - PQRSTUEABCDEFGHIJKLMNOPADJUFFUGZBUFZQUHRSTUIADCBEUJZGFHJIKLMNOQABIUFGUGZD - UFZPUHAVGVJKCUFRUKAEULUFVHULUFSEUMUNVJVGUOZVIVFVHUPZUQZUOAVGVJUOZVFVIEUPZ - UQZUOKLURVKVNVMVPVJVGUSVLVOVIVFEGUTFUTVAVBVCTVDUIVE $. - $} - - ${ - $d j k A $. $d j k B $. $d j k C $. $d j k G $. $d j k ph $. - gsumcom3fi.b $e |- B = ( Base ` G ) $. - gsumcom3fi.g $e |- ( ph -> G e. CMnd ) $. - gsumcom3fi.a $e |- ( ph -> A e. Fin ) $. - gsumcom3fi.r $e |- ( ph -> C e. Fin ) $. - gsumcom3fi.f $e |- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B ) $. - $( A commutative law for finite iterated sums. (Contributed by Stefan - O'Rear, 5-Sep-2015.) $) - gsumcom3fi $p |- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> - X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) ) $= - ( cxp cfn c0g cfv wcel cv wa eqid xpfi syl2anc wbr wn wceq biimpri adantl - brxp pm2.24d impr gsumcom3 ) ABCDBDNZEFGOOHGPQZIUNUAJKLMABORDORUMORKLBDUB - UCAESZBRFSZDRTZUOUPUMUDZUEHUNUFZAUQTURUSUQURAURUQUOUPBDUIUGUHUJUKUL $. - $} - ${ mamucl.b $e |- B = ( Base ` R ) $. mamucl.r $e |- ( ph -> R e. Ring ) $. @@ -469490,10 +469843,9 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a ${ slmdbn0.b $e |- B = ( Base ` W ) $. $( The base set of a semimodule is nonempty. (Contributed by Thierry - Arnoux, 1-Apr-2018.) $) + Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) $) slmdbn0 $p |- ( W e. SLMod -> B =/= (/) ) $= - ( cslmd wcel cmnd c0g cfv c0 wne slmdmnd eqid mndidcl ne0i 3syl ) BDEBFEB - GHZAEAIJBKABPCPLMAPNO $. + ( cslmd wcel cmnd c0 wne slmdmnd mndbn0 syl ) BDEBFEAGHBIABCJK $. $} ${ @@ -469523,10 +469875,10 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a slmdsn0.f $e |- F = ( Scalar ` W ) $. slmdsn0.b $e |- B = ( Base ` F ) $. $( The set of scalars in a semimodule is nonempty. (Contributed by Thierry - Arnoux, 1-Apr-2018.) $) + Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) $) slmdsn0 $p |- ( W e. SLMod -> B =/= (/) ) $= - ( cslmd wcel c0g cfv csrg cmnd slmdsrg srgmnd eqid mndidcl 3syl ne0d ) CF - GZABHIZRBJGBKGSAGBCDLBMABSESNOPQ $. + ( cslmd wcel csrg cmnd c0 wne slmdsrg srgmnd mndbn0 3syl ) CFGBHGBIGAJKBC + DLBMABENO $. $} ${ @@ -736488,48 +736840,6 @@ their group (addition) operations are equal for all pairs of elements of NULUMJUEHUCSSUFAFGMUKUSUGIBCUPFGUNUPTUNTUHUIUJ $. $} - ${ - $d B x $. $d L x $. $d R x $. $d .+ x $. - lidrideqd.l $e |- ( ph -> L e. B ) $. - lidrideqd.r $e |- ( ph -> R e. B ) $. - lidrideqd.li $e |- ( ph -> A. x e. B ( L .+ x ) = x ) $. - lidrideqd.ri $e |- ( ph -> A. x e. B ( x .+ R ) = x ) $. - $( If there is a left and right identity element for any binary operation - (group operation) ` .+ ` , both identity elements are equal. - Generalization of statement in [Lang] p. 3: it is sufficient that "e" is - a left identity element and "e``" is a right identity element instead of - both being (two-sided) identity elements. (Contributed by AV, - 26-Dec-2023.) $) - lidrideqd $p |- ( ph -> L = R ) $= - ( co cv wceq oveq1 id eqeq12d rspcdva oveq2 eqtr3d ) AFEDKZFEABLZEDKZUAMT - FMBCFUAFMZUBTUAFUAFEDNUCOPJGQAFUADKZUAMTEMBCEUAEMZUDTUAEUAEFDRUEOPIHQS $. - - $d B x y $. $d L y $. $d R y $. $d G y $. $d .+ y $. $d .0. y $. - $d ph y $. - lidrideqd.b $e |- B = ( Base ` G ) $. - lidrideqd.p $e |- .+ = ( +g ` G ) $. - lidrididd.o $e |- .0. = ( 0g ` G ) $. - $( If there is a left and right identity element for any binary operation - (group operation) ` .+ ` , the left identity element (and therefore also - the right identity element according to ~ lidrideqd ) is equal to the - two-sided identity element. (Contributed by AV, 26-Dec-2023.) $) - lidrididd $p |- ( ph -> L = .0. ) $= - ( vy cv co wceq wral wcel oveq2 id eqeq12d rspcv mpan9 wi lidrideqd oveq1 - weq wa adantl simpl eqtrd ex syl6com com23 sylc imp ismgmid2 ) APCDGFHMON - IAGBQZDRZVASZBCTPQZCUAZGVDDRZVDSZKVCVGBVDCBPUJZVBVFVAVDVAVDGDUBVHUCZUDUEU - FAVEVDGDRZVDSZAVAEDRZVASZBCTZGESZVEVKUGLABCDEGIJKLUHVNVEVOVKVEVNVDEDRZVDS - ZVOVKUGVMVQBVDCVHVLVPVAVDVAVDEDUIVIUDUEVQVOVKVQVOUKVJVPVDVOVJVPSVQGEVDDUB - ULVQVOUMUNUOUPUQURUSUT $. - $} - - ${ - mndbn0.b $e |- B = ( Base ` G ) $. - $( The base set of a monoid is not empty. Statement in [Lang] p. 3. - (Contributed by AV, 29-Dec-2023.) $) - mndbn0 $p |- ( G e. Mnd -> B =/= (/) ) $= - ( cmnd wcel c0g cfv eqid mndidcl ne0d ) BDEABFGZABKCKHIJ $. - $} - $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -737180,92 +737490,6 @@ Group sum operation (extension 1) -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d F x $. $d M x $. $d N x $. $d ph x $. - gsumsplit1r.b $e |- B = ( Base ` G ) $. - gsumsplit1r.p $e |- .+ = ( +g ` G ) $. - gsumsplit1r.g $e |- ( ph -> G e. V ) $. - gsumsplit1r.m $e |- ( ph -> M e. ZZ ) $. - gsumsplit1r.n $e |- ( ph -> N e. ( ZZ>= ` M ) ) $. - gsumsplit1r.f $e |- ( ph -> F : ( M ... ( N + 1 ) ) --> B ) $. - $( Splitting off the rightmost summand of a group sum. This corresponds to - the (inductive) definition of a (finite) product in [Lang] p. 4, first - formula. (Contributed by AV, 26-Dec-2023.) $) - gsumsplit1r $p |- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` ( M ... N ) ) ) - .+ ( F ` ( N + 1 ) ) ) ) $= - ( vx co cfv cfz wcel syl cgsu caddc cseq cres cuz peano2uz gsumval2 seqp1 - c1 wceq wss fzssp1 a1i fssresd uzidd cz eluzfz1 fvresd eqtrd cv wa fzp1ss - seq1 sselda seqfveq2 eqtr2d oveq1d 3eqtrd ) AEDUAPGUIUBPZCDFUCZQZGVJQZVID - QZCPZEDFGRPZUDZUAPZVMCPABCDEFVIHIJKAGFUEQZSZVIVRSMFGUFTNUGAVSVKVNUJMCDFGU - HTAVLVQVMCAVQGCVPFUCZQVLABCVPEFGHIJKMAFVIRPZBVODNVOWAUKAFGULUMUNUGACOVPDF - FGAFLUOAFVTQZFVPQZFDQAFUPSZWBWCUJLCVPFVCTAFVODAVSFVOSMFGUQTURUSMAOUTZFUIU - BPGRPZSVAWEVODAWFVOWEAWDWFVOUKLFGVBTVDURVEVFVGVH $. - $} - - ${ - $d x y z B $. $d x y z G $. $d x y z .+ $. $d x y z W $. $d x y z X $. - gsumsgrpccat.b $e |- B = ( Base ` G ) $. - gsumsgrpccat.p $e |- .+ = ( +g ` G ) $. - $( Homomorphic property of not empty composites of a group sum over a - semigroup. Formerly part of proof for ~ gsumccat . (Contributed by AV, - 26-Dec-2023.) $) - gsumsgrpccat $p |- ( ( G e. SGrp /\ ( W e. Word B /\ X e. Word B ) - /\ ( W =/= (/) /\ X =/= (/) ) ) - -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) $= - ( wcel wa cfv caddc co c1 cmin cc0 cseq wceq cn0 syl wf vx vy csgrp cword - vz c0 wne chash cconcat cgsu simp1 cmgm sgrpmgm mgmcl syl3an1 3expb sylan - w3a cv sgrpass cuz cn lennncl ad2ant2r 3adant1 nnzd uzidd nnm1nn0 uzaddcl - ad2ant2l syl2anc nncnd 1cnd addsubassd ax-1cn npcan sylancl 3eltr4d nn0uz - cc fveq2d syl6eleq cfz cfzo ccatcl 3ad2ant2 wrdf ccatlen oveq2d cz fzoval - zaddcld eqtrd feq2d mpbid seqsplit simpl2l simpl2r eleq2d biimpar syl3anc - ffvelrnda ccatval1 seqfveq addid2d eqtr4d seqeq1d addcomd addsubd fveq12d - oveq1d ccatval3 eqcomd seqshft2 oveq12d nnaddcld gsumval2 simp2l 3eqtr4d - simp2r ) CUCHZDAUDZHZEYBHZIZDUFUGZEUFUGZIZURZDUHJZEUHJZKLZMNLZBDEUILZOPZJ - ZYJMNLZBDOPJZYKMNLZBEOPJZBLZCYNUJLCDUJLZCEUJLZBLYIYPYQYOJZYMBYNYQMKLZPZJZ - BLUUAYIUAUBUEBAYNOYQYMYIYAUAUSZAHZUBUSZAHZIUUHUUJBLZAHZYAYEYHUKZYAUUIUUKU - UMYACULHUUIUUKUUMCUMACUUHUUJBFGUNUOUPUQYIYAUUIUUKUEUSZAHURUULUUOBLUUHUUJU - UOBLBLQUUNACUUHUUJBUUOFGUTUQYIYJYSKLZYJVAJZYMUUEVAJYIYJUUQHYSRHZUUPUUQHYI - YJYIYJYEYHYJVBHZYAYCYFUUSYDYGADVCVDVEZVFZVGYIYKVBHZUURYEYHUVBYAYDYGUVBYCY - FAEVCVJVEZYKVHSZYSYJYJVIVKYIYJYKMYIYJUUTVLZYIYKUVCVLZYIVMZVNYIUUEYJVAYIYJ - VTHMVTHUUEYJQUVEVOYJMVPVQZWAVRYIYQROVAJZYIUUSYQRHUUTYJVHSVSWBZYIOYMWCLZAU - UHYNYIOYNUHJZWDLZAYNTZUVKAYNTYIYNYBHZUVNYEYAUVOYHADEWEWFAYNWGSYIUVMUVKAYN - YIUVMOYLWDLZUVKYIUVLYLOWDYEYAUVLYLQYHADEWHWFWIYIYLWJHUVPUVKQYIYJYKUVAYIYK - UVCVFZWLOYLWKSWMWNWOZXBWPYIUUDYRUUGYTBYIBUAYNDOYQUVJYIUUHOYQWCLZHZIYCYDUU - HOYJWDLZHZUUHYNJUUHDJQYCYDYAYHUVTWQYCYDYAYHUVTWRYIUWBUVTYIUWAUVSUUHYIYJWJ - HUWAUVSQUVAOYJWKSZWSWTADEUUHXCXAXDYIUUGYSYJKLZBYNOYJKLZPZJYTYIYMUWDUUFUWF - YIUUEUWEBYNYIUUEYJUWEUVHYIYJUVEXEXFXGYIYMYKYJKLZMNLUWDYIYLUWGMNYIYJYKUVEU - VFXHXKYIYKYJMUVFUVEUVGXIWMXJYIBUAEYNYJOYSYIYSRUVIUVDVSWBZUVAYIUUHOYSWCLZH - ZIZUUHYJKLYNJZUUHEJZUWKYCYDUUHOYKWDLZHZUWLUWMQYCYDYAYHUWJWQYCYDYAYHUWJWRY - IUWOUWJYIUWNUWIUUHYIYKWJHUWNUWIQUVQOYKWKSZWSWTADEUUHXLXAXMXNXFXOWMYIABYNC - OYMUCFGUUNYIYMRUVIYIYLVBHYMRHYIYJYKUUTUVCXPYLVHSVSWBUVRXQYIUUBYRUUCYTBYIA - BDCOYQUCFGUUNUVJYIUWAADTZUVSADTYIYCUWQYAYCYDYHXRADWGSYIUWAUVSADUWCWNWOXQY - IABECOYSUCFGUUNUWHYIUWNAETZUWIAETYIYDUWRYAYCYDYHXTAEWGSYIUWNUWIAEUWPWNWOX - QXOXS $. - $} - - ${ - gsumccatNEW.b $e |- B = ( Base ` G ) $. - gsumccatNEW.p $e |- .+ = ( +g ` G ) $. - $( Homomorphic property of composites. Second formula in [Lang] p. 4. - (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario - Carneiro, 1-Oct-2015.) (Proof shortened by AV, 26-Dec-2023.) - (Proof modification is discouraged.) TODO: will replace ~ gsumccat . $) - gsumccatNEW $p |- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> - ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) $= - ( wcel cconcat co cgsu wceq c0 oveq2d oveq2 syl6eq eqeq12d wne ad2antrr - wa cmnd cword w3a c0g cfv oveq1 eqid gsum0 oveq1d mndsgrp 3ad2ant1 3simpc - csgrp simpr anim1i gsumsgrpccat syl3anc simpl2 ccatrid syl simpl1 gsumwcl - 3adant3 adantr mndrid syl2anc eqtr4d pm2.61ne ccatlid 3ad2ant3 3imp3i2an - simp1 mndlid ) CUAHZDAUBZHZEVOHZUCZCDEIJZKJZCDKJZCEKJZBJZLZCMEIJZKJZCUDUE - ZWBBJZLDMDMLZVTWFWCWHWIVSWECKDMEIUFNWIWAWGWBBWIWACMKJZWGDMCKOCWGWGUGZUHZP - UIQVRDMRZTZWDCDMIJZKJZWAWGBJZLEMEMLZVTWPWCWQWRVSWOCKEMDIONWRWBWGWABWRWBWJ - WGEMCKOWLPNQWNEMRZTCUMHZVPVQTZWMWSTWDVRWTWMWSVNVPWTVQCUJUKSVRXAWMWSVNVPVQ - ULSWNWMWSVRWMUNUOABCDEFGUPUQWNWPWAWQWNWODCKWNVPWODLVNVPVQWMURADUSUTNWNVNW - AAHZWQWALVNVPVQWMVAVRXBWMVNVPXBVQACDFVBVCVDABCWAWGFGWKVEVFVGVHVRWFWBWHVRW - EECKVQVNWEELVPAEVIVJNVNVPVQVNWBAHWHWBLVNVPVQVLACEFVBABCWBWGFGWKVMVKVGVH - $. - $} - ${ $d k A $. $d k B $. $d k C $. $d k D $. gsumsplit2f.n $e |- F/ k ph $. @@ -737312,20 +737536,6 @@ Group sum operation (extension 1) $. $} - ${ - gsumreidx.b $e |- B = ( Base ` G ) $. - gsumreidx.z $e |- .0. = ( 0g ` G ) $. - gsumreidx.g $e |- ( ph -> G e. CMnd ) $. - gsumreidx.f $e |- ( ph -> F : ( M ... N ) --> B ) $. - gsumreidx.h $e |- ( ph -> H : ( M ... N ) -1-1-onto-> ( M ... N ) ) $. - $( Re-index a finite group sum using a bijection. Corresponds to the first - equation in [Lang] p. 5 with ` M = 1 ` . (Contributed by AV, - 26-Dec-2023.) $) - gsumreidx $p |- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) $= - ( cfz co cvv ovexd fzfid wcel c0g fvexi a1i fdmfifsupp gsumf1o ) AFGNOZBU - ECDEPHIJKAFGNQLAUEBCPHLAFGRHPSAHDTJUAUBUCMUD $. - $} - ${ gsumfsupp.b $e |- B = ( Base ` G ) $. gsumfsupp.z $e |- .0. = ( 0g ` G ) $. @@ -737342,155 +737552,6 @@ corresponds to the definition of an (infinite) product in [Lang] p. 5, ( csupp co wss eqimss2i a1i gsumres ) ABCDEGFHIJLMNDHPQZFRAFUBKSTOUA $. $} - ${ - $d A j k $. $d B j k $. $d C j k $. $d G j k $. $d F j k $. $d V j $. - $d W k $. $d .0. j k $. $d ph j k $. - gsumxp2.b $e |- B = ( Base ` G ) $. - gsumxp2.z $e |- .0. = ( 0g ` G ) $. - gsumxp2.g $e |- ( ph -> G e. CMnd ) $. - gsumxp2.a $e |- ( ph -> A e. V ) $. - gsumxp2.r $e |- ( ph -> C e. W ) $. - gsumxp2.f $e |- ( ph -> F : ( A X. C ) --> B ) $. - gsumxp2.w $e |- ( ph -> F finSupp .0. ) $. - $( Write a group sum over a cartesian product as a double sum in two ways. - This corresponds to the first equation in [Lang] p. 6. (Contributed by - AV, 27-Dec-2023.) $) - gsumxp2 $p |- ( ph - -> ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> ( j F k ) ) ) ) ) - = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) ) $= - ( co wcel cv cmpt cgsu csupp fovrnda fsuppimpd wa wbr wn wceq cop cfv cxp - simpl opelxpi ad2antlr simpr eldifd cvv ssidd xpexd c0g fvexi a1i suppssr - cdif syl2an2r ex df-br notbii df-ov eqeq1i 3imtr4g impr gsumcom3 eqcomd ) - AHEBHFDEUAZFUAZGSZUBUCSUBUCSHFDHEBVSUBUCSUBUCSABCDGKUDSZEFHIJVSKLMNOPAVQV - RCBDGQUEAGKRUFAVQBTVRDTUGZVQVRVTUHZUIZVSKUJZAWAUGZVQVRUKZVTTZUIZWFGULZKUJ - ZWCWDWEWHWJWEAWHWFBDUMZVTVFTWJAWAUNWEWHUGWFWKVTWAWFWKTAWHVQVRBDUOUPWEWHUQ - URAWKCUSGUSVTWFKQAVTUTABDIJOPVAKUSTAKHVBMVCVDVEVGVHWBWGVQVRVTVIVJVSWIKVQV - RGVKVLVMVNVOVP $. - $} - - -$( --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- - Group multiple operation (extension) and cyclic monoids --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- -$) - - ${ - $d B i x $. $d F i $. $d N i x $. $d X i x $. - mulgnngsum.b $e |- B = ( Base ` G ) $. - mulgnngsum.t $e |- .x. = ( .g ` G ) $. - mulgnngsum.f $e |- F = ( x e. ( 1 ... N ) |-> X ) $. - $( Group multiple (exponentiation) operation at a positive integer - expressed by a group sum. (Contributed by AV, 28-Dec-2023.) $) - mulgnngsum $p |- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) ) $= - ( vi cn wcel wa cfv c1 cseq co adantr cv cplusg csn cxp cuz elnnuz biimpi - cgsu cfz cmpt wceq a1i eqidd simpr fvmptd elfznn fvconst2g syl2an seqfveq - weq eqtr4d cvv eqid elfvex eleq2s adantl fmptd gsumval2 mulgnn 3eqtr4rd - cbs ) FLMZGBMZNZFEUAOZDPQOFVNLGUBUCZPQZOEDUGRFGCRVMVNKDVOPFVKFPUDOMZVLVKV - QFUEUFSZVMKTZPFUHRZMZNZVSDOGVSVOOZWBAVSGGVTDBDAVTGUIUJWBJUKWBAKUSNGULVMWA - UMVMVLWAVKVLUMZSUNVMVLVSLMWCGUJWAWDVSFUOLGVSBUPUQUTURVMBVNDEPFVAHVNVBZVLE - VAMZVKWFGEVJOBGEVJVCHVDVEVRVMAVTGBDVMVLATVTMWDSJVFVGBVNVPCEFGHWEIVPVBVHVI - $. - - $( Group multiple (exponentiation) operation at a nonnegative integer - expressed by a groups sum. This corresponds to the definition in [Lang] - p. 6, second formula. (Contributed by AV, 28-Dec-2023.) $) - mulgnn0gsum $p |- ( ( N e. NN0 /\ X e. B ) - -> ( N .x. X ) = ( G gsum F ) ) $= - ( wcel co cgsu wceq cc0 ex c0 c1 cfz syl6eq cn0 cn wo wi elnn0 mulgnngsum - wa c0g cfv oveq1 eqid mulg0 sylan9eq cmpt oveq2 fz10 eqidd mpteq12dv mpt0 - syl5eq adantr oveq2d gsum0 eqtr4d jaoi sylbi imp ) FUAKZGBKZFGCLZEDMLZNZV - HFUBKZFONZUCVIVLUDZFUEVMVOVNVMVIVLABCDEFGHIJUFPVNVIVLVNVIUGZVJEUHUIZVKVNV - IVJOGCLVQFOGCUJBCEGVQHVQUKZIULUMVPVKEQMLVQVPDQEMVNDQNVIVNDARFSLZGUNZQJVNV - TAQGUNQVNAVSGQGVNVSROSLQFORSUOUPTVNGUQURAGUSTUTVAVBEVQVRVCTVDPVEVFVG $. - $} - - ${ - $d A x $. $d F i $. $d X i $. $d i x $. $d .x. x $. - cycsubm.b $e |- B = ( Base ` G ) $. - cycsubm.t $e |- .x. = ( .g ` G ) $. - cycsubm.f $e |- F = ( x e. NN0 |-> ( x .x. A ) ) $. - cycsubm.c $e |- C = ran F $. - $( Characterization of an element of the set of nonnegative integer powers - of an element ` A ` . Although this theorem holds for any class ` G ` , - the definition of ` F ` is only meaningful if ` G ` is a monoid or at - least a unital magma. (Contributed by AV, 28-Dec-2023.) $) - cycsubmel $p |- ( X e. C <-> E. i e. NN0 X = ( i .x. A ) ) $= - ( wcel cv wceq cn0 wrex co ovex crn cfv eleq2i wfn wb fvelrnb ax-mp oveq1 - fnmpti fvmpt eqeq1d eqcom syl6bb rexbiia 3bitri ) IDNIGUAZNZFOZGUBZIPZFQR - ZIURBESZPZFQRDUPIMUCGQUDUQVAUEAQAOZBESZGVDBETLUIFQIGUFUGUTVCFQURQNZUTVBIP - VCVFUSVBIAURVEVBQGVDURBEUHLURBETUJUKVBIULUMUNUO $. - - $d A i $. $d B i $. $d .x. i $. - $( The set of nonnegative integer powers of an element ` A ` contains - ` A ` . Although this theorem holds for any class ` G ` , the - definition of ` F ` is only meaningful if ` G ` is a monoid or at least - a unital magma. (Contributed by AV, 28-Dec-2023.) $) - cycsubmcl $p |- ( A e. B -> A e. C ) $= - ( vi wcel cv co wceq cn0 wrex c1 1nn0 wb oveq1 eqeq2d adantl mulg1 eqcomd - a1i rspcedvd cycsubmel sylibr ) BCMZBLNZBEOZPZLQRBDMUKUNBSBEOZPZLSQSQMUKT - UGULSPZUNUPUAUKUQUMUOBULSBEUBUCUDUKUOBCEGBHIUEUFUHABCDELFGBHIJKUIUJ $. - - $d A a b j k $. $d B a b j k x $. $d C a b $. $d F j k $. - $d G a b i j k x $. $d .x. j k $. - $( The set of nonnegative integer powers of an element ` A ` of a monoid - forms a submonoid containing ` A ` ( see ~ cycsubmcl ), called the - cyclic monoid generated by the element ` A ` . This corresponds to the - statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.) $) - cycsubm $p |- ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) ) $= - ( va vi wcel wa cv co cn0 wceq cc0 vb vj vk cmnd csubmnd cfv wss c0g wral - cplusg crn mulgnn0cl 3expa an32s fmptd frnd eqsstrid wrex 0nn0 a1i eqeq2d - wb oveq1 adantl mulg0 eqcomd rspcedvd cycsubmel sylibr caddc simplr simpr - eqid wi nn0addcld adantr oveq12 ancoms simplll simpllr syl13anc sylan9eqr - mulgnn0dir exp32 rexlimdva com23 impd anbi12i 3imtr4g ralrimivv mpbir3and - w3a issubm ) GUDNZBCNZOZDGUEUFNZDCUGZGUHUFZDNZLPZUAPZGUJUFZQZDNZUADUILDUI - ZWPDFUKCKWPRCFWPARAPZBEQZCFWNXGRNZWOXHCNZWNXIWOXJCEGXGBHIULUMUNJUOUPUQWPW - SMPZBEQZSZMRURWTWPXMWSTBEQZSZMTRTRNWPUSUTXKTSZXMXOVBWPXPXLXNWSXKTBEVCVAVD - WPXNWSWOXNWSSWNCEGBWSHWSVMZIVEVDVFVGABCDEMFGWSHIJKVHVIWPXELUADDWPXAXLSZMR - URZXBUBPZBEQZSZUBRURZOXDUCPZBEQZSZUCRURZXADNZXBDNZOXEWPXSYCYGWPXRYCYGVNMR - WPXKRNZOZYCXRYGYKYBXRYGVNUBRYKXTRNZOZYBXRYGYMYBXROZOZYFXDXKXTVJQZBEQZSZUC - YPRYMYPRNYNYMXKXTWPYJYLVKZYKYLVLZVOVPYDYPSZYFYRVBYOUUAYEYQXDYDYPBEVCVAVDY - NYMXDXLYAXCQZYQXRYBXDUUBSXAXLXBYAXCVQVRYMYQUUBYMWNYJYLWOYQUUBSWNWOYJYLVSY - SYTWNWOYJYLVTCXCEGXKXTBHIXCVMZWCWAVFWBVGWDWEWFWEWGYHXSYIYCABCDEMFGXAHIJKV - HABCDEUBFGXBHIJKVHWHABCDEUCFGXDHIJKVHWIWJWNWQWRWTXFWLVBWOLUACXCDGWSHXQUUC - WMVPWK $. - $} - - -$( --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- - Direct products (extension) --.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- -$) - - ${ - $d G x y $. $d U x y $. - smndlsmidm.p $e |- .(+) = ( LSSum ` G ) $. - $( The direct product is idempotent for submonoids. (Contributed by AV, - 27-Dec-2023.) $) - smndlsmidm $p |- ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = U ) $= - ( vx vy csubmnd cfv wcel co cv cplusg cmpo crn cdm cbs wss wceq eqid wral - elfvdm submss lsmvalx syl3anc cxp submcl 3expb ralrimivva fmpo sylib frnd - wf eqsstrd lsmub1x mpancom eqssd ) BCGHIZBBAJZBUQUREFBBEKZFKZCLHZJZMZNZBU - QCGOZIBCPHZQZVGURVDRBCGUAVFBCVFSZUBZVIEFVFVAABBCVEVHVASZDUCUDUQBBUEZBVCUQ - VBBIZFBTEBTVKBVCULUQVLEFBBUQUSBIUTBIVLVABCUSUTVJUFUGUHEFBBVBBVCVCSUIUJUKU - MVGUQBURQVIVFABBCVHDUNUOUP $. - - $( Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised - by Mario Carneiro, 21-Jun-2014.) (Proof shortened by AV, 27-Dec-2023.) - (Proof modification is discouraged.) $) - lsmidmNEW $p |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) $= - ( csubg cfv wcel csubmnd co wceq subgsubm smndlsmidm syl ) BCEFGBCHFGBBAI - BJBCKABCDLM $. - - mndlsmidm.b $e |- B = ( Base ` G ) $. - $( Subgroup sum is idempotent for monoids. This corresponds to the - observation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) $) - mndlsmidm $p |- ( G e. Mnd -> ( B .(+) B ) = B ) $= - ( cmnd wcel csubmnd cfv co wceq submid smndlsmidm syl ) CFGACHIGAABJAKACE - LBACDMN $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=