![]() |
Metamath
Proof Explorer Theorem List (p. 198 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqgabl 19701 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ βΌ = (πΊ ~QG π) β β’ ((πΊ β Abel β§ π β π) β (π΄ βΌ π΅ β (π΄ β π β§ π΅ β π β§ (π΅ β π΄) β π))) | ||
Theorem | qusecsub 19702 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ βΌ = (πΊ ~QG π) β β’ (((πΊ β Abel β§ π β (SubGrpβπΊ)) β§ (π β π΅ β§ π β π΅)) β ([π] βΌ = [π] βΌ β (π β π) β π)) | ||
Theorem | subgabl 19703 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ)) β π» β Abel) | ||
Theorem | subcmn 19704 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β CMnd β§ π» β Mnd) β π» β CMnd) | ||
Theorem | submcmn 19705 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β CMnd β§ π β (SubMndβπΊ)) β π» β CMnd) | ||
Theorem | submcmn2 19706 | A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π» = (πΊ βΎs π) & β’ π = (CntzβπΊ) β β’ (π β (SubMndβπΊ) β (π» β CMnd β π β (πβπ))) | ||
Theorem | cntzcmn 19707 | The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) β β’ ((πΊ β CMnd β§ π β π΅) β (πβπ) = π΅) | ||
Theorem | cntzcmnss 19708 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) β β’ ((πΊ β CMnd β§ π β π΅) β π β (πβπ)) | ||
Theorem | cntrcmnd 19709 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβπ)) β β’ (π β Mnd β π β CMnd) | ||
Theorem | cntrabl 19710 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβπ)) β β’ (π β Grp β π β Abel) | ||
Theorem | cntzspan 19711 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ πΎ = (mrClsβ(SubMndβπΊ)) & β’ π» = (πΊ βΎs (πΎβπ)) β β’ ((πΊ β Mnd β§ π β (πβπ)) β π» β CMnd) | ||
Theorem | cntzcmnf 19712 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β ran πΉ β (πβran πΉ)) | ||
Theorem | ghmplusg 19713 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ + = (+gβπ) β β’ ((π β Abel β§ πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ βf + πΊ) β (π GrpHom π)) | ||
Theorem | ablnsg 19714 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (πΊ β Abel β (NrmSGrpβπΊ) = (SubGrpβπΊ)) | ||
Theorem | odadd1 19715 | The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (odβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Abel β§ π΄ β π β§ π΅ β π) β ((πβ(π΄ + π΅)) Β· ((πβπ΄) gcd (πβπ΅))) β₯ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | odadd2 19716 | The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (odβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Abel β§ π΄ β π β§ π΅ β π) β ((πβπ΄) Β· (πβπ΅)) β₯ ((πβ(π΄ + π΅)) Β· (((πβπ΄) gcd (πβπ΅))β2))) | ||
Theorem | odadd 19717 | The order of a product is the product of the orders, if the factors have coprime order. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (odβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (((πΊ β Abel β§ π΄ β π β§ π΅ β π) β§ ((πβπ΄) gcd (πβπ΅)) = 1) β (πβ(π΄ + π΅)) = ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | gex2abl 19718 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ ((πΊ β Grp β§ πΈ β₯ 2) β πΊ β Abel) | ||
Theorem | gexexlem 19719* | Lemma for gexex 19720. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) & β’ π = (odβπΊ) & β’ (π β πΊ β Abel) & β’ (π β πΈ β β) & β’ (π β π΄ β π) & β’ ((π β§ π¦ β π) β (πβπ¦) β€ (πβπ΄)) β β’ (π β (πβπ΄) = πΈ) | ||
Theorem | gexex 19720* | In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if πΈ = 0, for example in an infinite p-group, where there are elements of arbitrarily large orders (so πΈ is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) & β’ π = (odβπΊ) β β’ ((πΊ β Abel β§ πΈ β β) β βπ₯ β π (πβπ₯) = πΈ) | ||
Theorem | torsubg 19721 | The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (odβπΊ) β β’ (πΊ β Abel β (β‘π β β) β (SubGrpβπΊ)) | ||
Theorem | oddvdssubg 19722* | The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (odβπΊ) & β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Abel β§ π β β€) β {π₯ β π΅ β£ (πβπ₯) β₯ π} β (SubGrpβπΊ)) | ||
Theorem | lsmcomx 19723 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β (π β π) = (π β π)) | ||
Theorem | ablcntzd 19724 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) β β’ (π β π β (πβπ)) | ||
Theorem | lsmcom 19725 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) = (π β π)) | ||
Theorem | lsmsubg2 19726 | The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.) |
β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) β (SubGrpβπΊ)) | ||
Theorem | lsm4 19727 | Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ (π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β§ (π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ))) β ((π β π ) β (π β π)) = ((π β π) β (π β π))) | ||
Theorem | prdscmnd 19728 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆCMnd) β β’ (π β π β CMnd) | ||
Theorem | prdsabld 19729 | The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆAbel) β β’ (π β π β Abel) | ||
Theorem | pwscmn 19730 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β CMnd β§ πΌ β π) β π β CMnd) | ||
Theorem | pwsabl 19731 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Abel β§ πΌ β π) β π β Abel) | ||
Theorem | qusabl 19732 | If π is a subgroup of the abelian group πΊ, then π» = πΊ / π is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π» = (πΊ /s (πΊ ~QG π)) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ)) β π» β Abel) | ||
Theorem | abl1 19733 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Abel) | ||
Theorem | abln0 19734 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
β’ Abel β β | ||
Theorem | cnaddablx 19735 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19736 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 19736 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
β’ πΊ = {β¨1, ββ©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | cnaddabl 19736 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19735 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 20966. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ πΊ β Abel | ||
Theorem | cnaddid 19737 | The group identity element of complex number addition is zero. See also cnfld0 20968. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ (0gβπΊ) = 0 | ||
Theorem | cnaddinv 19738 | Value of the group inverse of complex number addition. See also cnfldneg 20970. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ (π΄ β β β ((invgβπΊ)βπ΄) = -π΄) | ||
Theorem | zaddablx 19739 | The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg 20997 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
β’ πΊ = {β¨1, β€β©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | frgpnabllem1 19740* | Lemma for frgpnabl 19742. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
β’ πΊ = (freeGrpβπΌ) & β’ π = ( I βWord (πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) & β’ + = (+gβπΊ) & β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) & β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) & β’ π· = (π β βͺ π₯ β π ran (πβπ₯)) & β’ π = (varFGrpβπΌ) & β’ (π β πΌ β π) & β’ (π β π΄ β πΌ) & β’ (π β π΅ β πΌ) β β’ (π β β¨ββ¨π΄, β β©β¨π΅, β β©ββ© β (π· β© ((πβπ΄) + (πβπ΅)))) | ||
Theorem | frgpnabllem2 19741* | Lemma for frgpnabl 19742. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
β’ πΊ = (freeGrpβπΌ) & β’ π = ( I βWord (πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) & β’ + = (+gβπΊ) & β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) & β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) & β’ π· = (π β βͺ π₯ β π ran (πβπ₯)) & β’ π = (varFGrpβπΌ) & β’ (π β πΌ β π) & β’ (π β π΄ β πΌ) & β’ (π β π΅ β πΌ) & β’ (π β ((πβπ΄) + (πβπ΅)) = ((πβπ΅) + (πβπ΄))) β β’ (π β π΄ = π΅) | ||
Theorem | frgpnabl 19742 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ πΊ = (freeGrpβπΌ) β β’ (1o βΊ πΌ β Β¬ πΊ β Abel) | ||
Theorem | imasabl 19743* | The image structure of an abelian group is an abelian group (imasgrp 18938 analog). (Contributed by AV, 22-Feb-2025.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Abel) & β’ 0 = (0gβπ ) β β’ (π β (π β Abel β§ (πΉβ 0 ) = (0gβπ))) | ||
Syntax | ccyg 19744 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 19745* | Define a cyclic group, which is a group with an element π₯, called the generator of the group, such that all elements in the group are multiples of π₯. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ CycGrp = {π β Grp β£ βπ₯ β (Baseβπ)ran (π β β€ β¦ (π(.gβπ)π₯)) = (Baseβπ)} | ||
Theorem | iscyg 19746* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ ran (π β β€ β¦ (π Β· π₯)) = π΅)) | ||
Theorem | iscyggen 19747* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (π β πΈ β (π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅)) | ||
Theorem | iscyggen2 19748* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β Grp β (π β πΈ β (π β π΅ β§ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π)))) | ||
Theorem | iscyg2 19749* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β CycGrp β (πΊ β Grp β§ πΈ β β )) | ||
Theorem | cyggeninv 19750* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ π = (invgβπΊ) β β’ ((πΊ β Grp β§ π β πΈ) β (πβπ) β πΈ) | ||
Theorem | cyggenod 19751* | An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ π = (odβπΊ) β β’ ((πΊ β Grp β§ π΅ β Fin) β (π β πΈ β (π β π΅ β§ (πβπ) = (β―βπ΅)))) | ||
Theorem | cyggenod2 19752* | In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ π = (odβπΊ) β β’ ((πΊ β Grp β§ π β πΈ) β (πβπ) = if(π΅ β Fin, (β―βπ΅), 0)) | ||
Theorem | iscyg3 19753* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π₯))) | ||
Theorem | iscygd 19754* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) β β’ (π β πΊ β CycGrp) | ||
Theorem | iscygodd 19755 | Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β (πβπ) = (β―βπ΅)) β β’ (π β πΊ β CycGrp) | ||
Theorem | cycsubmcmn 19756* | The set of nonnegative integer powers of an element π΄ of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) & β’ πΆ = ran πΉ β β’ ((πΊ β Mnd β§ π΄ β π΅) β (πΊ βΎs πΆ) β CMnd) | ||
Theorem | cyggrp 19757 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ β CycGrp β πΊ β Grp) | ||
Theorem | cygabl 19758 | A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 20-Jan-2024.) |
β’ (πΊ β CycGrp β πΊ β Abel) | ||
Theorem | cygctb 19759 | A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β CycGrp β π΅ βΌ Ο) | ||
Theorem | 0cyg 19760 | The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ π΅ β 1o) β πΊ β CycGrp) | ||
Theorem | prmcyg 19761 | A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) β β) β πΊ β CycGrp) | ||
Theorem | lt6abl 19762 | A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) < 6) β πΊ β Abel) | ||
Theorem | ghmcyg 19763 | The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = (Baseβπ») β β’ ((πΉ β (πΊ GrpHom π») β§ πΉ:π΅βontoβπΆ) β (πΊ β CycGrp β π» β CycGrp)) | ||
Theorem | cyggex2 19764 | The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ (πΊ β CycGrp β πΈ = if(π΅ β Fin, (β―βπ΅), 0)) | ||
Theorem | cyggex 19765 | The exponent of a finite cyclic group is the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ ((πΊ β CycGrp β§ π΅ β Fin) β πΈ = (β―βπ΅)) | ||
Theorem | cyggexb 19766 | A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ ((πΊ β Abel β§ π΅ β Fin) β (πΊ β CycGrp β πΈ = (β―βπ΅))) | ||
Theorem | giccyg 19767 | Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ βπ π» β (πΊ β CycGrp β π» β CycGrp)) | ||
Theorem | cycsubgcyg 19768* | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ π = ran (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΊ βΎs π) β CycGrp) | ||
Theorem | cycsubgcyg2 19769 | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π΅) β (πΊ βΎs (πΎβ{π΄})) β CycGrp) | ||
Theorem | gsumval3a 19770* | Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by AV, 29-May-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β π β Fin) & β’ (π β π β β ) & β’ π = (πΉ supp 0 ) & β’ (π β Β¬ π΄ β ran ...) β β’ (π β (πΊ Ξ£g πΉ) = (β©π₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ))))) | ||
Theorem | gsumval3eu 19771* | The group sum as defined in gsumval3a 19770 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β π β Fin) & β’ (π β π β β ) & β’ (π β π β π΄) β β’ (π β β!π₯βπ(π:(1...(β―βπ))β1-1-ontoβπ β§ π₯ = (seq1( + , (πΉ β π))β(β―βπ)))) | ||
Theorem | gsumval3lem1 19772* | Lemma 1 for gsumval3 19774. (Contributed by AV, 31-May-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β π β β) & β’ (π β π»:(1...π)β1-1βπ΄) & β’ (π β (πΉ supp 0 ) β ran π») & β’ π = ((πΉ β π») supp 0 ) β β’ (((π β§ π β β ) β§ (Β¬ π΄ β ran ... β§ π Isom < , < ((1...(β―βπ)), π))) β (π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) | ||
Theorem | gsumval3lem2 19773* | Lemma 2 for gsumval3 19774. (Contributed by AV, 31-May-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β π β β) & β’ (π β π»:(1...π)β1-1βπ΄) & β’ (π β (πΉ supp 0 ) β ran π») & β’ π = ((πΉ β π») supp 0 ) β β’ (((π β§ π β β ) β§ (Β¬ π΄ β ran ... β§ π Isom < , < ((1...(β―βπ)), π))) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ))) | ||
Theorem | gsumval3 19774 | Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β π β β) & β’ (π β π»:(1...π)β1-1βπ΄) & β’ (π β (πΉ supp 0 ) β ran π») & β’ π = ((πΉ β π») supp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) | ||
Theorem | gsumcllem 19775* | Lemma for gsumcl 19782 and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (πΉ supp π) β π) β β’ ((π β§ π = β ) β πΉ = (π β π΄ β¦ π)) | ||
Theorem | gsumzres 19776 | Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β (πΉ supp 0 ) β π) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βΎ π)) = (πΊ Ξ£g πΉ)) | ||
Theorem | gsumzcl2 19777 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 19778, because it is not required that πΉ is a function (actually, the hypothesis always holds for any proper class πΉ). (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β (πΉ supp 0 ) β Fin) β β’ (π β (πΊ Ξ£g πΉ) β π΅) | ||
Theorem | gsumzcl 19778 | Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β π΅) | ||
Theorem | gsumzf1o 19779 | Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 2-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) & β’ (π β π»:πΆβ1-1-ontoβπ΄) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) | ||
Theorem | gsumres 19780 | Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp 0 ) β π) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βΎ π)) = (πΊ Ξ£g πΉ)) | ||
Theorem | gsumcl2 19781 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 19782, because it is not required that πΉ is a function (actually, the hypothesis always holds for any proper class πΉ). (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp 0 ) β Fin) β β’ (π β (πΊ Ξ£g πΉ) β π΅) | ||
Theorem | gsumcl 19782 | Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β π΅) | ||
Theorem | gsumf1o 19783 | Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ (π β π»:πΆβ1-1-ontoβπ΄) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) | ||
Theorem | gsumreidx 19784 | Re-index a finite group sum using a bijection. Corresponds to the first equation in [Lang] p. 5 with π = 1. (Contributed by AV, 26-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ:(π...π)βΆπ΅) & β’ (π β π»:(π...π)β1-1-ontoβ(π...π)) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) | ||
Theorem | gsumzsubmcl 19785 | Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β π β (SubMndβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β π) | ||
Theorem | gsumsubmcl 19786 | Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β π β (SubMndβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β π) | ||
Theorem | gsumsubgcl 19787 | Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β π) | ||
Theorem | gsumzaddlem 19788* | The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) & β’ π = ((πΉ βͺ π») supp 0 ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β ran π» β (πβran π»)) & β’ (π β ran (πΉ βf + π») β (πβran (πΉ βf + π»))) & β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πΉβπ) β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) β β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsumzadd 19789 | The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) & β’ (π β π β (SubMndβπΊ)) & β’ (π β π β (πβπ)) & β’ (π β πΉ:π΄βΆπ) & β’ (π β π»:π΄βΆπ) β β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsumadd 19790 | The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsummptfsadd 19791* | The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 9-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β π΅) & β’ (π β πΉ = (π₯ β π΄ β¦ πΆ)) & β’ (π β π» = (π₯ β π΄ β¦ π·)) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ (πΆ + π·))) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsummptfidmadd 19792* | The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β π΅) & β’ πΉ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ π·) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ (πΆ + π·))) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsummptfidmadd2 19793* | The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β π΅) & β’ πΉ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ π·) β β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsumzsplit 19794 | Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ πΆ)) + (πΊ Ξ£g (πΉ βΎ π·)))) | ||
Theorem | gsumsplit 19795 | Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ πΆ)) + (πΊ Ξ£g (πΉ βΎ π·)))) | ||
Theorem | gsumsplit2 19796* | Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β πΆ β¦ π)) + (πΊ Ξ£g (π β π· β¦ π)))) | ||
Theorem | gsummptfidmsplit 19797* | Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β πΆ β¦ π)) + (πΊ Ξ£g (π β π· β¦ π)))) | ||
Theorem | gsummptfidmsplitres 19798* | Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) & β’ πΉ = (π β π΄ β¦ π) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ πΆ)) + (πΊ Ξ£g (πΉ βΎ π·)))) | ||
Theorem | gsummptfzsplit 19799* | Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by AV, 25-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β β0) & β’ ((π β§ π β (0...(π + 1))) β π β π΅) β β’ (π β (πΊ Ξ£g (π β (0...(π + 1)) β¦ π)) = ((πΊ Ξ£g (π β (0...π) β¦ π)) + (πΊ Ξ£g (π β {(π + 1)} β¦ π)))) | ||
Theorem | gsummptfzsplitl 19800* | Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, , extracting a singleton from the left. (Contributed by AV, 7-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β β0) & β’ ((π β§ π β (0...π)) β π β π΅) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ π)) = ((πΊ Ξ£g (π β (1...π) β¦ π)) + (πΊ Ξ£g (π β {0} β¦ π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |