![]() |
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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | invghm 19701 | The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.) |
β’ π΅ = (BaseβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β Abel β πΌ β (πΊ GrpHom πΊ)) | ||
Theorem | eqgabl 19702 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ βΌ = (πΊ ~QG π) β β’ ((πΊ β Abel β§ π β π) β (π΄ βΌ π΅ β (π΄ β π β§ π΅ β π β§ (π΅ β π΄) β π))) | ||
Theorem | qusecsub 19703 | 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 19704 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ)) β π» β Abel) | ||
Theorem | subcmn 19705 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β CMnd β§ π» β Mnd) β π» β CMnd) | ||
Theorem | submcmn 19706 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β CMnd β§ π β (SubMndβπΊ)) β π» β CMnd) | ||
Theorem | submcmn2 19707 | 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 19708 | 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 19709 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) β β’ ((πΊ β CMnd β§ π β π΅) β π β (πβπ)) | ||
Theorem | cntrcmnd 19710 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβπ)) β β’ (π β Mnd β π β CMnd) | ||
Theorem | cntrabl 19711 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs (Cntrβπ)) β β’ (π β Grp β π β Abel) | ||
Theorem | cntzspan 19712 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ πΎ = (mrClsβ(SubMndβπΊ)) & β’ π» = (πΊ βΎs (πΎβπ)) β β’ ((πΊ β Mnd β§ π β (πβπ)) β π» β CMnd) | ||
Theorem | cntzcmnf 19713 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (CntzβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β ran πΉ β (πβran πΉ)) | ||
Theorem | ghmplusg 19714 | 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 19715 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (πΊ β Abel β (NrmSGrpβπΊ) = (SubGrpβπΊ)) | ||
Theorem | odadd1 19716 | 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 19717 | 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 19718 | 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 19719 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ ((πΊ β Grp β§ πΈ β₯ 2) β πΊ β Abel) | ||
Theorem | gexexlem 19720* | Lemma for gexex 19721. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) & β’ π = (odβπΊ) & β’ (π β πΊ β Abel) & β’ (π β πΈ β β) & β’ (π β π΄ β π) & β’ ((π β§ π¦ β π) β (πβπ¦) β€ (πβπ΄)) β β’ (π β (πβπ΄) = πΈ) | ||
Theorem | gexex 19721* | 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 19722 | 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 19723* | 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 19724 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β (π β π) = (π β π)) | ||
Theorem | ablcntzd 19725 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) β β’ (π β π β (πβπ)) | ||
Theorem | lsmcom 19726 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
β’ β = (LSSumβπΊ) β β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) = (π β π)) | ||
Theorem | lsmsubg2 19727 | 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 19728 | 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 19729 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆCMnd) β β’ (π β π β CMnd) | ||
Theorem | prdsabld 19730 | 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 19731 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β CMnd β§ πΌ β π) β π β CMnd) | ||
Theorem | pwsabl 19732 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Abel β§ πΌ β π) β π β Abel) | ||
Theorem | qusabl 19733 | 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 19734 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Abel) | ||
Theorem | abln0 19735 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
β’ Abel β β | ||
Theorem | cnaddablx 19736 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19737 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 19737 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
β’ πΊ = {β¨1, ββ©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | cnaddabl 19737 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19736 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 20967. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ πΊ β Abel | ||
Theorem | cnaddid 19738 | The group identity element of complex number addition is zero. See also cnfld0 20969. (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 19739 | Value of the group inverse of complex number addition. See also cnfldneg 20971. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), ββ©, β¨(+gβndx), + β©} β β’ (π΄ β β β ((invgβπΊ)βπ΄) = -π΄) | ||
Theorem | zaddablx 19740 | 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 20998 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
β’ πΊ = {β¨1, β€β©, β¨2, + β©} β β’ πΊ β Abel | ||
Theorem | frgpnabllem1 19741* | Lemma for frgpnabl 19743. (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 19742* | Lemma for frgpnabl 19743. (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 19743 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ πΊ = (freeGrpβπΌ) β β’ (1o βΊ πΌ β Β¬ πΊ β Abel) | ||
Theorem | imasabl 19744* | The image structure of an abelian group is an abelian group (imasgrp 18939 analog). (Contributed by AV, 22-Feb-2025.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Abel) & β’ 0 = (0gβπ ) β β’ (π β (π β Abel β§ (πΉβ 0 ) = (0gβπ))) | ||
Syntax | ccyg 19745 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 19746* | 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 19747* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ ran (π β β€ β¦ (π Β· π₯)) = π΅)) | ||
Theorem | iscyggen 19748* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (π β πΈ β (π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅)) | ||
Theorem | iscyggen2 19749* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β Grp β (π β πΈ β (π β π΅ β§ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π)))) | ||
Theorem | iscyg2 19750* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} β β’ (πΊ β CycGrp β (πΊ β Grp β§ πΈ β β )) | ||
Theorem | cyggeninv 19751* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ π = (invgβπΊ) β β’ ((πΊ β Grp β§ π β πΈ) β (πβπ) β πΈ) | ||
Theorem | cyggenod 19752* | 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 19753* | 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 19754* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β CycGrp β (πΊ β Grp β§ βπ₯ β π΅ βπ¦ β π΅ βπ β β€ π¦ = (π Β· π₯))) | ||
Theorem | iscygd 19755* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) β β’ (π β πΊ β CycGrp) | ||
Theorem | iscygodd 19756 | 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 19757* | 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 19758 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ β CycGrp β πΊ β Grp) | ||
Theorem | cygabl 19759 | A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 20-Jan-2024.) |
β’ (πΊ β CycGrp β πΊ β Abel) | ||
Theorem | cygctb 19760 | A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β CycGrp β π΅ βΌ Ο) | ||
Theorem | 0cyg 19761 | The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ π΅ β 1o) β πΊ β CycGrp) | ||
Theorem | prmcyg 19762 | A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) β β) β πΊ β CycGrp) | ||
Theorem | lt6abl 19763 | A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Grp β§ (β―βπ΅) < 6) β πΊ β Abel) | ||
Theorem | ghmcyg 19764 | 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 19765 | 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 19766 | 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 19767 | 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 19768 | Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ βπ π» β (πΊ β CycGrp β π» β CycGrp)) | ||
Theorem | cycsubgcyg 19769* | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ π = ran (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΊ βΎs π) β CycGrp) | ||
Theorem | cycsubgcyg2 19770 | The cyclic subgroup generated by π΄ is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π΅) β (πΊ βΎs (πΎβ{π΄})) β CycGrp) | ||
Theorem | gsumval3a 19771* | 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 19772* | The group sum as defined in gsumval3a 19771 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 19773* | Lemma 1 for gsumval3 19775. (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 19774* | Lemma 2 for gsumval3 19775. (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 19775 | 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 19776* | Lemma for gsumcl 19783 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 19777 | 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 19778 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 19779, 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 19779 | 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 19780 | 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 19781 | 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 19782 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 19783, 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 19783 | 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 19784 | 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 19785 | 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 19786 | 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 19787 | 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 19788 | 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 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 ) & β’ π = ((πΉ βͺ π») supp 0 ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β ran πΉ β (πβran πΉ)) & β’ (π β ran π» β (πβran π»)) & β’ (π β ran (πΉ βf + π») β (πβran (πΉ βf + π»))) & β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πΉβπ) β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) β β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) | ||
Theorem | gsumzadd 19790 | 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 19791 | 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 19792* | 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 19793* | 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 19794* | 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 19795 | 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 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 | gsumsplit2 19797* | 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 19798* | 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 19799* | 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 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 right. (Contributed by AV, 25-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β β0) & β’ ((π β§ π β (0...(π + 1))) β π β π΅) β β’ (π β (πΊ Ξ£g (π β (0...(π + 1)) β¦ π)) = ((πΊ Ξ£g (π β (0...π) β¦ π)) + (πΊ Ξ£g (π β {(π + 1)} β¦ π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |