![]() |
Metamath
Proof Explorer Theorem List (p. 200 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | telgsumfz0 19901* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15754. (Contributed by AV, 23-Nov-2019.) |
β’ πΎ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β β0) & β’ (π β βπ β (0...(π + 1))π΄ β πΎ) & β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = 0 β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ (π΅ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsums 19902* | 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 19903* | 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 β¦ (πΆ β π·))) = πΈ) | ||
Syntax | cdprd 19904 | Internal direct product of a family of subgroups. |
class DProd | ||
Syntax | cdpj 19905 | Projection operator for a direct product. |
class dProj | ||
Definition | df-dprd 19906* | Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ DProd = (π β Grp, π β {β β£ (β:dom ββΆ(SubGrpβπ) β§ βπ₯ β dom β(βπ¦ β (dom β β {π₯})(ββπ₯) β ((Cntzβπ)β(ββπ¦)) β§ ((ββπ₯) β© ((mrClsβ(SubGrpβπ))ββͺ (β β (dom β β {π₯})))) = {(0gβπ)}))} β¦ ran (π β {β β Xπ₯ β dom π (π βπ₯) β£ β finSupp (0gβπ)} β¦ (π Ξ£g π))) | ||
Definition | df-dpj 19907* | Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ dProj = (π β Grp, π β (dom DProd β {π}) β¦ (π β dom π β¦ ((π βπ)(proj1βπ)(π DProd (π βΎ (dom π β {π})))))) | ||
Theorem | reldmdprd 19908 | The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.) |
β’ Rel dom DProd | ||
Theorem | dmdprd 19909* | The domain of definition of the internal direct product, which states that π is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.) |
β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΌ β π β§ dom π = πΌ) β (πΊdom DProd π β (πΊ β Grp β§ π:πΌβΆ(SubGrpβπΊ) β§ βπ₯ β πΌ (βπ¦ β (πΌ β {π₯})(πβπ₯) β (πβ(πβπ¦)) β§ ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) = { 0 })))) | ||
Theorem | dmdprdd 19910* | Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ (π β πΊ β Grp) & β’ (π β πΌ β π) & β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ ((π β§ (π₯ β πΌ β§ π¦ β πΌ β§ π₯ β π¦)) β (πβπ₯) β (πβ(πβπ¦))) & β’ ((π β§ π₯ β πΌ) β ((πβπ₯) β© (πΎββͺ (π β (πΌ β {π₯})))) β { 0 }) β β’ (π β πΊdom DProd π) | ||
Theorem | dprddomprc 19911 | A family of subgroups indexed by a proper class cannot be a family of subgroups for an internal direct product. (Contributed by AV, 13-Jul-2019.) |
β’ (dom π β V β Β¬ πΊdom DProd π) | ||
Theorem | dprddomcld 19912 | If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) β β’ (π β πΌ β V) | ||
Theorem | dprdval0prc 19913 | The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019.) |
β’ (dom π β V β (πΊ DProd π) = β ) | ||
Theorem | dprdval 19914* | The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } β β’ ((πΊdom DProd π β§ dom π = πΌ) β (πΊ DProd π) = ran (π β π β¦ (πΊ Ξ£g π))) | ||
Theorem | eldprd 19915* | A class π΄ is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } β β’ (dom π = πΌ β (π΄ β (πΊ DProd π) β (πΊdom DProd π β§ βπ β π π΄ = (πΊ Ξ£g π)))) | ||
Theorem | dprdgrp 19916 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β πΊ β Grp) | ||
Theorem | dprdf 19917 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β π:dom πβΆ(SubGrpβπΊ)) | ||
Theorem | dprdf2 19918 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) β β’ (π β π:πΌβΆ(SubGrpβπΊ)) | ||
Theorem | dprdcntz 19919 | The function π is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πβπ))) | ||
Theorem | dprddisj 19920 | The function π is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ 0 = (0gβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (π β ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) = { 0 }) | ||
Theorem | dprdw 19921* | The property of being a finitely supported function in the family π. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) β β’ (π β (πΉ β π β (πΉ Fn πΌ β§ βπ₯ β πΌ (πΉβπ₯) β (πβπ₯) β§ πΉ finSupp 0 ))) | ||
Theorem | dprdwd 19922* | A mapping being a finitely supported function in the family π. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) (Proof shortened by OpenAI, 30-Mar-2020.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ ((π β§ π₯ β πΌ) β π΄ β (πβπ₯)) & β’ (π β (π₯ β πΌ β¦ π΄) finSupp 0 ) β β’ (π β (π₯ β πΌ β¦ π΄) β π) | ||
Theorem | dprdff 19923* | A finitely supported function in π is a function into the base. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ π΅ = (BaseβπΊ) β β’ (π β πΉ:πΌβΆπ΅) | ||
Theorem | dprdfcl 19924* | A finitely supported function in π has its π-th element in π(π). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) β β’ ((π β§ π β πΌ) β (πΉβπ) β (πβπ)) | ||
Theorem | dprdffsupp 19925* | A finitely supported function in π is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) β β’ (π β πΉ finSupp 0 ) | ||
Theorem | dprdfcntz 19926* | A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ π = (CntzβπΊ) β β’ (π β ran πΉ β (πβran πΉ)) | ||
Theorem | dprdssv 19927 | The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ DProd π) β π΅ | ||
Theorem | dprdfid 19928* | A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ (π β π΄ β (πβπ)) & β’ πΉ = (π β πΌ β¦ if(π = π, π΄, 0 )) β β’ (π β (πΉ β π β§ (πΊ Ξ£g πΉ) = π΄)) | ||
Theorem | eldprdi 19929* | The domain of definition of the internal direct product, which states that π is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) β β’ (π β (πΊ Ξ£g πΉ) β (πΊ DProd π)) | ||
Theorem | dprdfinv 19930* | Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ π = (invgβπΊ) β β’ (π β ((π β πΉ) β π β§ (πΊ Ξ£g (π β πΉ)) = (πβ(πΊ Ξ£g πΉ)))) | ||
Theorem | dprdfadd 19931* | Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ (π β π» β π) & β’ + = (+gβπΊ) β β’ (π β ((πΉ βf + π») β π β§ (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»)))) | ||
Theorem | dprdfsub 19932* | Take the difference of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ (π β π» β π) & β’ β = (-gβπΊ) β β’ (π β ((πΉ βf β π») β π β§ (πΊ Ξ£g (πΉ βf β π»)) = ((πΊ Ξ£g πΉ) β (πΊ Ξ£g π»)))) | ||
Theorem | dprdfeq0 19933* | The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) β β’ (π β ((πΊ Ξ£g πΉ) = 0 β πΉ = (π₯ β πΌ β¦ 0 ))) | ||
Theorem | dprdf11 19934* | Two group sums over a direct product that give the same value are equal as functions. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ β π) & β’ (π β π» β π) β β’ (π β ((πΊ Ξ£g πΉ) = (πΊ Ξ£g π») β πΉ = π»)) | ||
Theorem | dprdsubg 19935 | The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β (πΊ DProd π) β (SubGrpβπΊ)) | ||
Theorem | dprdub 19936 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πβπ) β (πΊ DProd π)) | ||
Theorem | dprdlub 19937* | The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β (SubGrpβπΊ)) & β’ ((π β§ π β πΌ) β (πβπ) β π) β β’ (π β (πΊ DProd π) β π) | ||
Theorem | dprdspan 19938 | The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (πΊdom DProd π β (πΊ DProd π) = (πΎββͺ ran π)) | ||
Theorem | dprdres 19939 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π΄ β πΌ) β β’ (π β (πΊdom DProd (π βΎ π΄) β§ (πΊ DProd (π βΎ π΄)) β (πΊ DProd π))) | ||
Theorem | dprdss 19940* | Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ ((π β§ π β πΌ) β (πβπ) β (πβπ)) β β’ (π β (πΊdom DProd π β§ (πΊ DProd π) β (πΊ DProd π))) | ||
Theorem | dprdz 19941* | A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ πΌ β π) β (πΊdom DProd (π₯ β πΌ β¦ { 0 }) β§ (πΊ DProd (π₯ β πΌ β¦ { 0 })) = { 0 })) | ||
Theorem | dprd0 19942 | The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β (πΊdom DProd β β§ (πΊ DProd β ) = { 0 })) | ||
Theorem | dprdf1o 19943 | Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ:π½β1-1-ontoβπΌ) β β’ (π β (πΊdom DProd (π β πΉ) β§ (πΊ DProd (π β πΉ)) = (πΊ DProd π))) | ||
Theorem | dprdf1 19944 | Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΉ:π½β1-1βπΌ) β β’ (π β (πΊdom DProd (π β πΉ) β§ (πΊ DProd (π β πΉ)) β (πΊ DProd π))) | ||
Theorem | subgdmdprd 19945 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) β β’ (π΄ β (SubGrpβπΊ) β (π»dom DProd π β (πΊdom DProd π β§ ran π β π« π΄))) | ||
Theorem | subgdprd 19946 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) & β’ (π β π΄ β (SubGrpβπΊ)) & β’ (π β πΊdom DProd π) & β’ (π β ran π β π« π΄) β β’ (π β (π» DProd π) = (πΊ DProd π)) | ||
Theorem | dprdsn 19947 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ ((π΄ β π β§ π β (SubGrpβπΊ)) β (πΊdom DProd {β¨π΄, πβ©} β§ (πΊ DProd {β¨π΄, πβ©}) = π)) | ||
Theorem | dmdprdsplitlem 19948* | Lemma for dmdprdsplit 19958. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π΄ β πΌ) & β’ (π β πΉ β π) & β’ (π β (πΊ Ξ£g πΉ) β (πΊ DProd (π βΎ π΄))) β β’ ((π β§ π β (πΌ β π΄)) β (πΉβπ) = 0 ) | ||
Theorem | dprdcntz2 19949 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΆ β πΌ) & β’ (π β π· β πΌ) & β’ (π β (πΆ β© π·) = β ) & β’ π = (CntzβπΊ) β β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) | ||
Theorem | dprddisj2 19950 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΆ β πΌ) & β’ (π β π· β πΌ) & β’ (π β (πΆ β© π·) = β ) & β’ 0 = (0gβπΊ) β β’ (π β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) | ||
Theorem | dprd2dlem2 19951* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β Rel π΄) & β’ (π β π:π΄βΆ(SubGrpβπΊ)) & β’ (π β dom π΄ β πΌ) & β’ ((π β§ π β πΌ) β πΊdom DProd (π β (π΄ β {π}) β¦ (πππ))) & β’ (π β πΊdom DProd (π β πΌ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ))))) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((π β§ π β π΄) β (πβπ) β (πΊ DProd (π β (π΄ β {(1st βπ)}) β¦ ((1st βπ)ππ)))) | ||
Theorem | dprd2dlem1 19952* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β Rel π΄) & β’ (π β π:π΄βΆ(SubGrpβπΊ)) & β’ (π β dom π΄ β πΌ) & β’ ((π β§ π β πΌ) β πΊdom DProd (π β (π΄ β {π}) β¦ (πππ))) & β’ (π β πΊdom DProd (π β πΌ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ))))) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ (π β πΆ β πΌ) β β’ (π β (πΎββͺ (π β (π΄ βΎ πΆ))) = (πΊ DProd (π β πΆ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ)))))) | ||
Theorem | dprd2da 19953* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β Rel π΄) & β’ (π β π:π΄βΆ(SubGrpβπΊ)) & β’ (π β dom π΄ β πΌ) & β’ ((π β§ π β πΌ) β πΊdom DProd (π β (π΄ β {π}) β¦ (πππ))) & β’ (π β πΊdom DProd (π β πΌ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ))))) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (π β πΊdom DProd π) | ||
Theorem | dprd2db 19954* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β Rel π΄) & β’ (π β π:π΄βΆ(SubGrpβπΊ)) & β’ (π β dom π΄ β πΌ) & β’ ((π β§ π β πΌ) β πΊdom DProd (π β (π΄ β {π}) β¦ (πππ))) & β’ (π β πΊdom DProd (π β πΌ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ))))) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (π β (πΊ DProd π) = (πΊ DProd (π β πΌ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ)))))) | ||
Theorem | dprd2d2 19955* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ ((π β§ (π β πΌ β§ π β π½)) β π β (SubGrpβπΊ)) & β’ ((π β§ π β πΌ) β πΊdom DProd (π β π½ β¦ π)) & β’ (π β πΊdom DProd (π β πΌ β¦ (πΊ DProd (π β π½ β¦ π)))) β β’ (π β (πΊdom DProd (π β πΌ, π β π½ β¦ π) β§ (πΊ DProd (π β πΌ, π β π½ β¦ π)) = (πΊ DProd (π β πΌ β¦ (πΊ DProd (π β π½ β¦ π)))))) | ||
Theorem | dmdprdsplit2lem 19956 | Lemma for dmdprdsplit 19958. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ (π β (πΆ β© π·) = β ) & β’ (π β πΌ = (πΆ βͺ π·)) & β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊdom DProd (π βΎ πΆ)) & β’ (π β πΊdom DProd (π βΎ π·)) & β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) & β’ (π β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((π β§ π β πΆ) β ((π β πΌ β (π β π β (πβπ) β (πβ(πβπ)))) β§ ((πβπ) β© (πΎββͺ (π β (πΌ β {π})))) β { 0 })) | ||
Theorem | dmdprdsplit2 19957 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ (π β (πΆ β© π·) = β ) & β’ (π β πΌ = (πΆ βͺ π·)) & β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊdom DProd (π βΎ πΆ)) & β’ (π β πΊdom DProd (π βΎ π·)) & β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) & β’ (π β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) β β’ (π β πΊdom DProd π) | ||
Theorem | dmdprdsplit 19958 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ (π β (πΆ β© π·) = β ) & β’ (π β πΌ = (πΆ βͺ π·)) & β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) β β’ (π β (πΊdom DProd π β ((πΊdom DProd (π βΎ πΆ) β§ πΊdom DProd (π βΎ π·)) β§ (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·))) β§ ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }))) | ||
Theorem | dprdsplit 19959 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β π:πΌβΆ(SubGrpβπΊ)) & β’ (π β (πΆ β© π·) = β ) & β’ (π β πΌ = (πΆ βͺ π·)) & β’ β = (LSSumβπΊ) & β’ (π β πΊdom DProd π) β β’ (π β (πΊ DProd π) = ((πΊ DProd (π βΎ πΆ)) β (πΊ DProd (π βΎ π·)))) | ||
Theorem | dmdprdpr 19960 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) β β’ (π β (πΊdom DProd {β¨β , πβ©, β¨1o, πβ©} β (π β (πβπ) β§ (π β© π) = { 0 }))) | ||
Theorem | dprdpr 19961 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π = (CntzβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) & β’ β = (LSSumβπΊ) & β’ (π β π β (πβπ)) & β’ (π β (π β© π) = { 0 }) β β’ (π β (πΊ DProd {β¨β , πβ©, β¨1o, πβ©}) = (π β π)) | ||
Theorem | dpjlem 19962 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πΊ DProd (π βΎ {π})) = (πβπ)) | ||
Theorem | dpjcntz 19963 | The two subgroups that appear in dpjval 19967 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πΊ DProd (π βΎ (πΌ β {π}))))) | ||
Theorem | dpjdisj 19964 | The two subgroups that appear in dpjval 19967 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ 0 = (0gβπΊ) β β’ (π β ((πβπ) β© (πΊ DProd (π βΎ (πΌ β {π})))) = { 0 }) | ||
Theorem | dpjlsm 19965 | The two subgroups that appear in dpjval 19967 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ β = (LSSumβπΊ) β β’ (π β (πΊ DProd π) = ((πβπ) β (πΊ DProd (π βΎ (πΌ β {π}))))) | ||
Theorem | dpjfval 19966* | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ π = (proj1βπΊ) β β’ (π β π = (π β πΌ β¦ ((πβπ)π(πΊ DProd (π βΎ (πΌ β {π})))))) | ||
Theorem | dpjval 19967 | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ π = (proj1βπΊ) & β’ (π β π β πΌ) β β’ (π β (πβπ) = ((πβπ)π(πΊ DProd (π βΎ (πΌ β {π}))))) | ||
Theorem | dpjf 19968 | The π-th index projection is a function from the direct product to the π-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π β πΌ) β β’ (π β (πβπ):(πΊ DProd π)βΆ(πβπ)) | ||
Theorem | dpjidcl 19969* | The key property of projections: the sum of all the projections of π΄ is π΄. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π΄ β (πΊ DProd π)) & β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } β β’ (π β ((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β π β§ π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄))))) | ||
Theorem | dpjeq 19970* | Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π΄ β (πΊ DProd π)) & β’ 0 = (0gβπΊ) & β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } & β’ (π β (π₯ β πΌ β¦ πΆ) β π) β β’ (π β (π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ πΆ)) β βπ₯ β πΌ ((πβπ₯)βπ΄) = πΆ)) | ||
Theorem | dpjid 19971* | The key property of projections: the sum of all the projections of π΄ is π΄. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π΄ β (πΊ DProd π)) β β’ (π β π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄)))) | ||
Theorem | dpjlid 19972 | The π-th index projection acts as the identity on elements of the π-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π β πΌ) & β’ (π β π΄ β (πβπ)) β β’ (π β ((πβπ)βπ΄) = π΄) | ||
Theorem | dpjrid 19973 | The π-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π β πΌ) & β’ (π β π΄ β (πβπ)) & β’ 0 = (0gβπΊ) & β’ (π β π β πΌ) & β’ (π β π β π) β β’ (π β ((πβπ)βπ΄) = 0 ) | ||
Theorem | dpjghm 19974 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π β πΌ) β β’ (π β (πβπ) β ((πΊ βΎs (πΊ DProd π)) GrpHom πΊ)) | ||
Theorem | dpjghm2 19975 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ π = (πΊdProjπ) & β’ (π β π β πΌ) β β’ (π β (πβπ) β ((πΊ βΎs (πΊ DProd π)) GrpHom (πΊ βΎs (πβπ)))) | ||
Theorem | ablfacrplem 19976* | Lemma for ablfacrp2 19978. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΎ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ πΏ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ (π β πΊ β Abel) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π gcd π) = 1) & β’ (π β (β―βπ΅) = (π Β· π)) β β’ (π β ((β―βπΎ) gcd π) = 1) | ||
Theorem | ablfacrp 19977* | A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups πΎ, πΏ that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΎ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ πΏ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ (π β πΊ β Abel) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π gcd π) = 1) & β’ (π β (β―βπ΅) = (π Β· π)) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) β β’ (π β ((πΎ β© πΏ) = { 0 } β§ (πΎ β πΏ) = π΅)) | ||
Theorem | ablfacrp2 19978* | The factors πΎ, πΏ of ablfacrp 19977 have the expected orders (which allows for repeated application to decompose πΊ into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΎ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ πΏ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ (π β πΊ β Abel) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π gcd π) = 1) & β’ (π β (β―βπ΅) = (π Β· π)) β β’ (π β ((β―βπΎ) = π β§ (β―βπΏ) = π)) | ||
Theorem | ablfac1lem 19979* | Lemma for ablfac1b 19981. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π = (πβ(π pCnt (β―βπ΅))) & β’ π = ((β―βπ΅) / π) β β’ ((π β§ π β π΄) β ((π β β β§ π β β) β§ (π gcd π) = 1 β§ (β―βπ΅) = (π Β· π))) | ||
Theorem | ablfac1a 19980* | The factors of ablfac1b 19981 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) β β’ ((π β§ π β π΄) β (β―β(πβπ)) = (πβ(π pCnt (β―βπ΅)))) | ||
Theorem | ablfac1b 19981* | Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) β β’ (π β πΊdom DProd π) | ||
Theorem | ablfac1c 19982* | The factors of ablfac1b 19981 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π· = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ (π β π· β π΄) β β’ (π β (πΊ DProd π) = π΅) | ||
Theorem | ablfac1eulem 19983* | Lemma for ablfac1eu 19984. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π· = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ (π β π· β π΄) & β’ (π β (πΊdom DProd π β§ (πΊ DProd π) = π΅)) & β’ (π β dom π = π΄) & β’ ((π β§ π β π΄) β πΆ β β0) & β’ ((π β§ π β π΄) β (β―β(πβπ)) = (πβπΆ)) & β’ (π β π β β) & β’ (π β π΄ β Fin) β β’ (π β Β¬ π β₯ (β―β(πΊ DProd (π βΎ (π΄ β {π}))))) | ||
Theorem | ablfac1eu 19984* | The factorization of ablfac1b 19981 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to π. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π· = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ (π β π· β π΄) & β’ (π β (πΊdom DProd π β§ (πΊ DProd π) = π΅)) & β’ (π β dom π = π΄) & β’ ((π β§ π β π΄) β πΆ β β0) & β’ ((π β§ π β π΄) β (β―β(πβπ)) = (πβπΆ)) β β’ (π β π = π) | ||
Theorem | pgpfac1lem1 19985* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) β β’ ((π β§ πΆ β (π β (π β π))) β ((π β π) β (πΎβ{πΆ})) = π) | ||
Theorem | pgpfac1lem2 19986* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) & β’ (π β πΆ β (π β (π β π))) & β’ Β· = (.gβπΊ) β β’ (π β (π Β· πΆ) β (π β π)) | ||
Theorem | pgpfac1lem3a 19987* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 4-Jun-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) & β’ (π β πΆ β (π β (π β π))) & β’ Β· = (.gβπΊ) & β’ (π β π β β€) & β’ (π β ((π Β· πΆ)(+gβπΊ)(π Β· π΄)) β π) β β’ (π β (π β₯ πΈ β§ π β₯ π)) | ||
Theorem | pgpfac1lem3 19988* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) & β’ (π β πΆ β (π β (π β π))) & β’ Β· = (.gβπΊ) & β’ (π β π β β€) & β’ (π β ((π Β· πΆ)(+gβπΊ)(π Β· π΄)) β π) & β’ π· = (πΆ(+gβπΊ)((π / π) Β· π΄)) β β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) | ||
Theorem | pgpfac1lem4 19989* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) & β’ (π β πΆ β (π β (π β π))) & β’ Β· = (.gβπΊ) β β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) | ||
Theorem | pgpfac1lem5 19990* | Lemma for pgpfac1 19991. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β βπ β (SubGrpβπΊ)((π β π β§ π΄ β π ) β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π ))) β β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π)) | ||
Theorem | pgpfac1 19991* | Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π΄ β π΅) β β’ (π β βπ‘ β (SubGrpβπΊ)((π β© π‘) = { 0 } β§ (π β π‘) = π΅)) | ||
Theorem | pgpfaclem1 19992* | Lemma for pgpfac 19995. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π pGrp πΊ) & β’ (π β π΅ β Fin) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β βπ‘ β (SubGrpβπΊ)(π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘))) & β’ π» = (πΊ βΎs π) & β’ πΎ = (mrClsβ(SubGrpβπ»)) & β’ π = (odβπ») & β’ πΈ = (gExβπ») & β’ 0 = (0gβπ») & β’ β = (LSSumβπ») & β’ (π β πΈ β 1) & β’ (π β π β π) & β’ (π β (πβπ) = πΈ) & β’ (π β π β (SubGrpβπ»)) & β’ (π β ((πΎβ{π}) β© π) = { 0 }) & β’ (π β ((πΎβ{π}) β π) = π) & β’ (π β π β Word πΆ) & β’ (π β πΊdom DProd π) & β’ (π β (πΊ DProd π) = π) & β’ π = (π ++ β¨β(πΎβ{π})ββ©) β β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) | ||
Theorem | pgpfaclem2 19993* | Lemma for pgpfac 19995. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π pGrp πΊ) & β’ (π β π΅ β Fin) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β βπ‘ β (SubGrpβπΊ)(π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘))) & β’ π» = (πΊ βΎs π) & β’ πΎ = (mrClsβ(SubGrpβπ»)) & β’ π = (odβπ») & β’ πΈ = (gExβπ») & β’ 0 = (0gβπ») & β’ β = (LSSumβπ») & β’ (π β πΈ β 1) & β’ (π β π β π) & β’ (π β (πβπ) = πΈ) & β’ (π β π β (SubGrpβπ»)) & β’ (π β ((πΎβ{π}) β© π) = { 0 }) & β’ (π β ((πΎβ{π}) β π) = π) β β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) | ||
Theorem | pgpfaclem3 19994* | Lemma for pgpfac 19995. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π pGrp πΊ) & β’ (π β π΅ β Fin) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β βπ‘ β (SubGrpβπΊ)(π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘))) β β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) | ||
Theorem | pgpfac 19995* | Full factorization of a finite abelian p-group, by iterating pgpfac1 19991. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π pGrp πΊ) & β’ (π β π΅ β Fin) β β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π΅)) | ||
Theorem | ablfaclem1 19996* | Lemma for ablfac 19999. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ π = (odβπΊ) & β’ π΄ = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ π = (π β (SubGrpβπΊ) β¦ {π β Word πΆ β£ (πΊdom DProd π β§ (πΊ DProd π ) = π)}) β β’ (π β (SubGrpβπΊ) β (πβπ) = {π β Word πΆ β£ (πΊdom DProd π β§ (πΊ DProd π ) = π)}) | ||
Theorem | ablfaclem2 19997* | Lemma for ablfac 19999. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ π = (odβπΊ) & β’ π΄ = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ π = (π β (SubGrpβπΊ) β¦ {π β Word πΆ β£ (πΊdom DProd π β§ (πΊ DProd π ) = π)}) & β’ (π β πΉ:π΄βΆWord πΆ) & β’ (π β βπ¦ β π΄ (πΉβπ¦) β (πβ(πβπ¦))) & β’ πΏ = βͺ π¦ β π΄ ({π¦} Γ dom (πΉβπ¦)) & β’ (π β π»:(0..^(β―βπΏ))β1-1-ontoβπΏ) β β’ (π β (πβπ΅) β β ) | ||
Theorem | ablfaclem3 19998* | Lemma for ablfac 19999. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ π = (odβπΊ) & β’ π΄ = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ π = (π β (SubGrpβπΊ) β¦ {π β Word πΆ β£ (πΊdom DProd π β§ (πΊ DProd π ) = π)}) β β’ (π β (πβπ΅) β β ) | ||
Theorem | ablfac 19999* | The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) β β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π΅)) | ||
Theorem | ablfac2 20000* | Choose generators for each cyclic group in ablfac 19999. (Contributed by Mario Carneiro, 28-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp )} & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ Β· = (.gβπΊ) & β’ π = (π β dom π€ β¦ ran (π β β€ β¦ (π Β· (π€βπ)))) β β’ (π β βπ€ β Word π΅(π:dom π€βΆπΆ β§ πΊdom DProd π β§ (πΊ DProd π) = π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |