![]() |
Metamath
Proof Explorer Theorem List (p. 199 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oddvdssubg 19801* | 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 19802 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β (π β π) = (π β π)) | ||
Theorem | ablcntzd 19803 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) β β’ (π β π β (πβπ)) | ||
Theorem | lsmcom 19804 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) = (π β π)) | ||
Theorem | lsmsubg2 19805 | 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 19806 | 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 19807 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆCMnd) β β’ (π β π β CMnd) | ||
Theorem | prdsabld 19808 | 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 19809 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β CMnd β§ πΌ β π) β π β CMnd) | ||
Theorem | pwsabl 19810 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Abel β§ πΌ β π) β π β Abel) | ||
Theorem | qusabl 19811 | 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 19812 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Abel) | ||
Theorem | abln0 19813 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
β’ Abel β β | ||
Theorem | cnaddablx 19814 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19815 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 19815 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
β’ πΊ = {β¨1, ββ©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | cnaddabl 19815 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19814 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 21305. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ πΊ β Abel | ||
Theorem | cnaddid 19816 | The group identity element of complex number addition is zero. See also cnfld0 21307. (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 19817 | Value of the group inverse of complex number addition. See also cnfldneg 21310. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ (π΄ β β β ((invgβπΊ)βπ΄) = -π΄) | ||
Theorem | zaddablx 19818 | 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 21340 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
β’ πΊ = {β¨1, β€β©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | frgpnabllem1 19819* | Lemma for frgpnabl 19821. (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 19820* | Lemma for frgpnabl 19821. (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 19821 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ πΊ = (freeGrpβπΌ) β β’ (1o βΊ πΌ β Β¬ πΊ β Abel) | ||
Theorem | imasabl 19822* | The image structure of an abelian group is an abelian group (imasgrp 19003 analog). (Contributed by AV, 22-Feb-2025.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Abel) & β’ 0 = (0gβπ ) β β’ (π β (π β Abel β§ (πΉβ 0 ) = (0gβπ))) | ||
Syntax | ccyg 19823 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 19824* | 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 19825* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ ran (π β β€ β¦ (π Β· π₯)) = π΅)) | ||
Theorem | iscyggen 19826* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (π β πΈ β (π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅)) | ||
Theorem | iscyggen2 19827* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β Grp β (π β πΈ β (π β π΅ β§ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π)))) | ||
Theorem | iscyg2 19828* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β CycGrp β (πΊ β Grp β§ πΈ β β )) | ||
Theorem | cyggeninv 19829* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ π = (invgβπΊ) β β’ ((πΊ β Grp β§ π β πΈ) β (πβπ) β πΈ) | ||
Theorem | cyggenod 19830* | 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 19831* | 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 19832* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π₯))) | ||
Theorem | iscygd 19833* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) β β’ (π β πΊ β CycGrp) | ||
Theorem | iscygodd 19834 | 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 19835* | 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 19836 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ β CycGrp β πΊ β Grp) | ||
Theorem | cygabl 19837 | A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 20-Jan-2024.) |
β’ (πΊ β CycGrp β πΊ β Abel) | ||
Theorem | cygctb 19838 | A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β CycGrp β π΅ βΌ Ο) | ||
Theorem | 0cyg 19839 | The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ π΅ β 1o) β πΊ β CycGrp) | ||
Theorem | prmcyg 19840 | A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) β β) β πΊ β CycGrp) | ||
Theorem | lt6abl 19841 | A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) < 6) β πΊ β Abel) | ||
Theorem | ghmcyg 19842 | 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 19843 | 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 19844 | 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 19845 | 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 19846 | Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ βπ π» β (πΊ β CycGrp β π» β CycGrp)) | ||
Theorem | cycsubgcyg 19847* | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ π = ran (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΊ βΎs π) β CycGrp) | ||
Theorem | cycsubgcyg2 19848 | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π΅) β (πΊ βΎs (πΎβ{π΄})) β CycGrp) | ||
Theorem | gsumval3a 19849* | 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 19850* | The group sum as defined in gsumval3a 19849 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 19851* | Lemma 1 for gsumval3 19853. (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 19852* | Lemma 2 for gsumval3 19853. (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 19853 | 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 19854* | Lemma for gsumcl 19861 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 19855 | 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 19856 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 19857, 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 19857 | 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 19858 | 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 19859 | 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 19860 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 19861, 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 19861 | 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 19862 | 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 19863 | 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 19864 | 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 19865 | 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 19866 | 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 19867* | 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 19868 | 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 19869 | 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 19870* | 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 19871* | 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 19872* | 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 19873 | 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 19874 | 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 19875* | 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 19876* | 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 19877* | 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 19878* | 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 19879* | 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} β¦ π)))) | ||
Theorem | gsumconst 19880* | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) | ||
Theorem | gsumconstf 19881* | Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) | ||
Theorem | gsummptshft 19882* | Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β π΅) & β’ (π = (π β πΎ) β π΄ = πΆ) β β’ (π β (πΊ Ξ£g (π β (π...π) β¦ π΄)) = (πΊ Ξ£g (π β ((π + πΎ)...(π + πΎ)) β¦ πΆ))) | ||
Theorem | gsumzmhm 19883 | Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π» β Mnd) & β’ (π β π΄ β π) & β’ (π β πΎ β (πΊ MndHom π»)) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ 0 = (0gβπΊ) & β’ (π β πΉ finSupp 0 ) β β’ (π β (π» Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) | ||
Theorem | gsummhm 19884 | Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π» β Mnd) & β’ (π β π΄ β π) & β’ (π β πΎ β (πΊ MndHom π»)) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (π» Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) | ||
Theorem | gsummhm2 19885* | Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π» β Mnd) & β’ (π β π΄ β π) & β’ (π β (π₯ β π΅ β¦ πΆ) β (πΊ MndHom π»)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π₯ = π β πΆ = π·) & β’ (π₯ = (πΊ Ξ£g (π β π΄ β¦ π)) β πΆ = πΈ) β β’ (π β (π» Ξ£g (π β π΄ β¦ π·)) = πΈ) | ||
Theorem | gsummptmhm 19886* | Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018.) (Revised by AV, 8-Sep-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π» β Mnd) & β’ (π β π΄ β π) & β’ (π β πΎ β (πΊ MndHom π»)) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ (π β (π₯ β π΄ β¦ πΆ) finSupp 0 ) β β’ (π β (π» Ξ£g (π₯ β π΄ β¦ (πΎβπΆ))) = (πΎβ(πΊ Ξ£g (π₯ β π΄ β¦ πΆ)))) | ||
Theorem | gsummulglem 19887* | Lemma for gsummulg 19888 and gsummulgz 19889. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π β πΊ β CMnd) & β’ (π β π β β€) & β’ (π β (πΊ β Abel β¨ π β β0)) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (πΊ Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | gsummulg 19888* | Nonnegative multiple of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π β πΊ β CMnd) & β’ (π β π β β0) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (πΊ Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | gsummulgz 19889* | Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π β πΊ β Abel) & β’ (π β π β β€) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (πΊ Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | gsumzoppg 19890 | The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ π = (oppgβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) β β’ (π β (π Ξ£g πΉ) = (πΊ Ξ£g πΉ)) | ||
Theorem | gsumzinv 19891 | Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ πΌ = (invgβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΌ β πΉ)) = (πΌβ(πΊ Ξ£g πΉ))) | ||
Theorem | gsuminv 19892 | Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 4-May-2015.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ πΌ = (invgβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΌ β πΉ)) = (πΌβ(πΊ Ξ£g πΉ))) | ||
Theorem | gsummptfidminv 19893* | Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ πΌ = (invgβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ πΉ = (π₯ β π΄ β¦ πΆ) β β’ (π β (πΊ Ξ£g (πΌ β πΉ)) = (πΌβ(πΊ Ξ£g πΉ))) | ||
Theorem | gsumsub 19894 | The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βf β π»)) = ((πΊ Ξ£g πΉ) β (πΊ Ξ£g π»))) | ||
Theorem | gsummptfssub 19895* | The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β π΅) & β’ (π β πΉ = (π₯ β π΄ β¦ πΆ)) & β’ (π β π» = (π₯ β π΄ β¦ π·)) & β’ (π β πΉ finSupp 0 ) & β’ (π β π» finSupp 0 ) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ (πΆ β π·))) = ((πΊ Ξ£g πΉ) β (πΊ Ξ£g π»))) | ||
Theorem | gsummptfidmsub 19896* | The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β π΅) & β’ πΉ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ π·) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ (πΆ β π·))) = ((πΊ Ξ£g πΉ) β (πΊ Ξ£g π»))) | ||
Theorem | gsumsnfd 19897* | Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π) & β’ (π β πΆ β π΅) & β’ ((π β§ π = π) β π΄ = πΆ) & β’ β²ππ & β’ β²ππΆ β β’ (π β (πΊ Ξ£g (π β {π} β¦ π΄)) = πΆ) | ||
Theorem | gsumsnd 19898* | Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π) & β’ (π β πΆ β π΅) & β’ ((π β§ π = π) β π΄ = πΆ) β β’ (π β (πΊ Ξ£g (π β {π} β¦ π΄)) = πΆ) | ||
Theorem | gsumsnf 19899* | Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
β’ β²ππΆ & β’ π΅ = (BaseβπΊ) & β’ (π = π β π΄ = πΆ) β β’ ((πΊ β Mnd β§ π β π β§ πΆ β π΅) β (πΊ Ξ£g (π β {π} β¦ π΄)) = πΆ) | ||
Theorem | gsumsn 19900* | Group sum of a singleton. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π = π β π΄ = πΆ) β β’ ((πΊ β Mnd β§ π β π β§ πΆ β π΅) β (πΊ Ξ£g (π β {π} β¦ π΄)) = πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |