Home | Metamath
Proof Explorer Theorem List (p. 197 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lt6abl 19601 | A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) < 6) β πΊ β Abel) | ||
Theorem | ghmcyg 19602 | 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 19603 | 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 19604 | 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 19605 | 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 19606 | Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ βπ π» β (πΊ β CycGrp β π» β CycGrp)) | ||
Theorem | cycsubgcyg 19607* | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ π = ran (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΊ βΎs π) β CycGrp) | ||
Theorem | cycsubgcyg2 19608 | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π΅) β (πΊ βΎs (πΎβ{π΄})) β CycGrp) | ||
Theorem | gsumval3a 19609* | 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 19610* | The group sum as defined in gsumval3a 19609 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 19611* | Lemma 1 for gsumval3 19613. (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 19612* | Lemma 2 for gsumval3 19613. (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 19613 | 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 19614* | Lemma for gsumcl 19621 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 19615 | 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 19616 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 19617, 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 19617 | 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 19618 | 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 19619 | 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 19620 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 19621, 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 19621 | 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 19622 | 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 19623 | 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 19624 | 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 19625 | 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 19626 | 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 19627* | 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 19628 | 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 19629 | 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 19630* | 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 19631* | 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 19632* | 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 19633 | 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 19634 | 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 19635* | 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 19636* | 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 19637* | 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 19638* | 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 19639* | 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 19640* | 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 19641* | Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) | ||
Theorem | gsummptshft 19642* | 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 19643 | 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 19644 | 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 19645* | 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 19646* | 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 19647* | Lemma for gsummulg 19648 and gsummulgz 19649. (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 19648* | 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 19649* | 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 19650 | 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 19651 | 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 19652 | 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 19653* | 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 19654 | 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 19655* | 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 19656* | 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 19657* | 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 19658* | 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 19659* | 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 19660* | 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 (π β {π} β¦ π΄)) = πΆ) | ||
Theorem | gsumpr 19661* | Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π = π β π΄ = πΆ) & β’ (π = π β π΄ = π·) β β’ ((πΊ β CMnd β§ (π β π β§ π β π β§ π β π) β§ (πΆ β π΅ β§ π· β π΅)) β (πΊ Ξ£g (π β {π, π} β¦ π΄)) = (πΆ + π·)) | ||
Theorem | gsumzunsnd 19662* | Append an element to a finite group sum, more general version of gsumunsnd 19664. (Contributed by AV, 7-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ πΉ = (π β (π΄ βͺ {π}) β¦ π) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β Fin) & β’ (π β ran πΉ β (πβran πΉ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnfd 19663* | Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) & β’ β²ππ β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnd 19664* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 2-Jan-2019.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnf 19665* | Append an element to a finite group sum, 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βπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ (π = π β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsn 19666* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Proof shortened by AV, 8-Mar-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ (π = π β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumdifsnd 19667* | Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β (π β π΄ β¦ π) finSupp (0gβπΊ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β (π΄ β {π}) β¦ π)) + π)) | ||
Theorem | gsumpt 19668 | Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp 0 ) β {π}) β β’ (π β (πΊ Ξ£g πΉ) = (πΉβπ)) | ||
Theorem | gsummptf1o 19669* | Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.) |
β’ β²π₯π» & β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π₯ = πΈ β πΆ = π») & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΉ β π΅) & β’ ((π β§ π₯ β π΄) β πΆ β πΉ) & β’ ((π β§ π¦ β π·) β πΈ β π΄) & β’ ((π β§ π₯ β π΄) β β!π¦ β π· π₯ = πΈ) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ πΆ)) = (πΊ Ξ£g (π¦ β π· β¦ π»))) | ||
Theorem | gsummptun 19670* | Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β CMnd) & β’ (π β (π΄ βͺ πΆ) β Fin) & β’ (π β (π΄ β© πΆ) = β ) & β’ ((π β§ π₯ β (π΄ βͺ πΆ)) β π· β π΅) β β’ (π β (π Ξ£g (π₯ β (π΄ βͺ πΆ) β¦ π·)) = ((π Ξ£g (π₯ β π΄ β¦ π·)) + (π Ξ£g (π₯ β πΆ β¦ π·)))) | ||
Theorem | gsummpt1n0 19671* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 19672. (Contributed by AV, 11-Oct-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ πΉ = (π β πΌ β¦ if(π = π, π΄, 0 )) & β’ (π β βπ β πΌ π΄ β (BaseβπΊ)) β β’ (π β (πΊ Ξ£g πΉ) = β¦π / πβ¦π΄) | ||
Theorem | gsummptif1n0 19672* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019.) (Proof shortened by AV, 11-Oct-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ πΉ = (π β πΌ β¦ if(π = π, π΄, 0 )) & β’ (π β π΄ β (BaseβπΊ)) β β’ (π β (πΊ Ξ£g πΉ) = π΄) | ||
Theorem | gsummptcl 19673* | Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β Fin) & β’ (π β βπ β π π β π΅) β β’ (π β (πΊ Ξ£g (π β π β¦ π)) β π΅) | ||
Theorem | gsummptfif1o 19674* | Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β Fin) & β’ (π β βπ β π π β π΅) & β’ πΉ = (π β π β¦ π) & β’ (π β π»:πΆβ1-1-ontoβπ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) | ||
Theorem | gsummptfzcl 19675* | Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΌ = (π...π)) & β’ (π β βπ β πΌ π β π΅) β β’ (π β (πΊ Ξ£g (π β πΌ β¦ π)) β π΅) | ||
Theorem | gsum2dlem1 19676* | Lemma 1 for gsum2d 19678. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ))) β π΅) | ||
Theorem | gsum2dlem2 19677* | Lemma for gsum2d 19678. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βΎ (π΄ βΎ dom (πΉ supp 0 )))) = (πΊ Ξ£g (π β dom (πΉ supp 0 ) β¦ (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ)))))) | ||
Theorem | gsum2d 19678* | Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β π· β¦ (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ)))))) | ||
Theorem | gsum2d2lem 19679* | Lemma for gsum2d2 19680: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (π β π΄, π β πΆ β¦ π) finSupp 0 ) | ||
Theorem | gsum2d2 19680* | Write a group sum over a two-dimensional region as a double sum. Note that πΆ(π) is a function of π. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π))))) | ||
Theorem | gsumcom2 19681* | Two-dimensional commutation of a group sum. Note that while π΄ and π· are constants w.r.t. π, π, πΆ(π) and πΈ(π) are not. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) & β’ (π β π· β π) & β’ (π β ((π β π΄ β§ π β πΆ) β (π β π· β§ π β πΈ))) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β π·, π β πΈ β¦ π))) | ||
Theorem | gsumxp 19682* | Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ (ππΉπ)))))) | ||
Theorem | gsumcom 19683* | Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β πΆ, π β π΄ β¦ π))) | ||
Theorem | gsumcom3 19684* | A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π)))) = (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ π))))) | ||
Theorem | gsumcom3fi 19685* | A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΆ β Fin) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π)))) = (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ π))))) | ||
Theorem | gsumxp2 19686* | 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.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ (ππΉπ))))) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ (ππΉπ)))))) | ||
Theorem | prdsgsum 19687* | Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β π) & β’ ((π β§ π₯ β πΌ) β π β CMnd) & β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β π΅) & β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) β β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π Ξ£g (π¦ β π½ β¦ π)))) | ||
Theorem | pwsgsum 19688* | Finite commutative sums in a power structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β CMnd) & β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β π΅) & β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) β β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π Ξ£g (π¦ β π½ β¦ π)))) | ||
Theorem | fsfnn0gsumfsffz 19689* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β π β β0) & β’ π» = (πΉ βΎ (0...π)) β β’ (π β (βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 ) β (πΊ Ξ£g πΉ) = (πΊ Ξ£g π»))) | ||
Theorem | nn0gsumfz 19690* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β πΉ finSupp 0 ) β β’ (π β βπ β β0 βπ β (π΅ βm (0...π ))(π = (πΉ βΎ (0...π )) β§ βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 ) β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) | ||
Theorem | nn0gsumfz0 19691* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β πΉ finSupp 0 ) β β’ (π β βπ β β0 βπ β (π΅ βm (0...π ))(πΊ Ξ£g πΉ) = (πΊ Ξ£g π)) | ||
Theorem | gsummptnn0fz 19692* | A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 3-Jul-2022.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β βπ β β0 πΆ β π΅) & β’ (π β π β β0) & β’ (π β βπ β β0 (π < π β πΆ = 0 )) β β’ (π β (πΊ Ξ£g (π β β0 β¦ πΆ)) = (πΊ Ξ£g (π β (0...π) β¦ πΆ))) | ||
Theorem | gsummptnn0fzfv 19693* | A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β π β β0) & β’ (π β βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 )) β β’ (π β (πΊ Ξ£g (π β β0 β¦ (πΉβπ))) = (πΊ Ξ£g (π β (0...π) β¦ (πΉβπ)))) | ||
Theorem | telgsumfzslem 19694* | Lemma for telgsumfzs 19695 (induction step). (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) β β’ ((π¦ β (β€β₯βπ) β§ (π β§ βπ β (π...((π¦ + 1) + 1))πΆ β π΅)) β ((πΊ Ξ£g (π β (π...π¦) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦(π¦ + 1) / πβ¦πΆ) β (πΊ Ξ£g (π β (π...(π¦ + 1)) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦((π¦ + 1) + 1) / πβ¦πΆ))) | ||
Theorem | telgsumfzs 19695* | Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β (β€β₯βπ)) & β’ (π β βπ β (π...(π + 1))πΆ β π΅) β β’ (π β (πΊ Ξ£g (π β (π...π) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ)) | ||
Theorem | telgsumfz 19696* | Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15624. (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β (β€β₯βπ)) & β’ (π β βπ β (π...(π + 1))π΄ β π΅) & β’ (π = π β π΄ = πΏ) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (π...π) β¦ (πΏ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsumfz0s 19697* | Telescoping finite group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) (Proof shortened by AV, 25-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β β0) & β’ (π β βπ β (0...(π + 1))πΆ β π΅) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦0 / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ)) | ||
Theorem | telgsumfz0 19698* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15624. (Contributed by AV, 23-Nov-2019.) |
β’ πΎ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β β0) & β’ (π β βπ β (0...(π + 1))π΄ β πΎ) & β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = 0 β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ (π΅ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsums 19699* | Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β βπ β β0 πΆ β π΅) & β’ (π β π β β0) & β’ (π β βπ β β0 (π < π β πΆ = 0 )) β β’ (π β (πΊ Ξ£g (π β β0 β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = β¦0 / πβ¦πΆ) | ||
Theorem | telgsum 19700* | Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β βπ β β0 π΄ β π΅) & β’ (π β π β β0) & β’ (π β βπ β β0 (π < π β π΄ = 0 )) & β’ (π = π β π΄ = πΆ) & β’ (π = (π + 1) β π΄ = π·) & β’ (π = 0 β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β β0 β¦ (πΆ β π·))) = πΈ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |