![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | telgsumfz0s 19901* | 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 19902* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15755. (Contributed by AV, 23-Nov-2019.) |
β’ πΎ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β β0) & β’ (π β βπ β (0...(π + 1))π΄ β πΎ) & β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = 0 β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ (π΅ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsums 19903* | 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 19904* | 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 19905 | Internal direct product of a family of subgroups. |
class DProd | ||
Syntax | cdpj 19906 | Projection operator for a direct product. |
class dProj | ||
Definition | df-dprd 19907* | 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 19908* | 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 19909 | 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 19910* | 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 19911* | 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 19912 | 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 19913 | 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 19914 | 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 19915* | 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 19916* | 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 19917 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β πΊ β Grp) | ||
Theorem | dprdf 19918 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β π:dom πβΆ(SubGrpβπΊ)) | ||
Theorem | dprdf2 19919 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) β β’ (π β π:πΌβΆ(SubGrpβπΊ)) | ||
Theorem | dprdcntz 19920 | The function π is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πβπ))) | ||
Theorem | dprddisj 19921 | 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 19922* | 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 19923* | 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 19924* | 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 19925* | 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 19926* | 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 19927* | 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 19928 | 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 19929* | 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 19930* | 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 19931* | 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 19932* | 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 19933* | 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 19934* | 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 19935* | 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 19936 | 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 19937 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πβπ) β (πΊ DProd π)) | ||
Theorem | dprdlub 19938* | 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 19939 | 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 19940 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π΄ β πΌ) β β’ (π β (πΊdom DProd (π βΎ π΄) β§ (πΊ DProd (π βΎ π΄)) β (πΊ DProd π))) | ||
Theorem | dprdss 19941* | 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 19942* | 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 19943 | 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 19944 | 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 19945 | 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 19946 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) β β’ (π΄ β (SubGrpβπΊ) β (π»dom DProd π β (πΊdom DProd π β§ ran π β π« π΄))) | ||
Theorem | subgdprd 19947 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) & β’ (π β π΄ β (SubGrpβπΊ)) & β’ (π β πΊdom DProd π) & β’ (π β ran π β π« π΄) β β’ (π β (π» DProd π) = (πΊ DProd π)) | ||
Theorem | dprdsn 19948 | 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 19949* | Lemma for dmdprdsplit 19959. (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 19950 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΆ β πΌ) & β’ (π β π· β πΌ) & β’ (π β (πΆ β© π·) = β ) & β’ π = (CntzβπΊ) β β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) | ||
Theorem | dprddisj2 19951 | 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 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 (π β (π΄ β {(1st βπ)}) β¦ ((1st βπ)ππ)))) | ||
Theorem | dprd2dlem1 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βπΊ)) & β’ (π β πΆ β πΌ) β β’ (π β (πΎββͺ (π β (π΄ βΎ πΆ))) = (πΊ DProd (π β πΆ β¦ (πΊ DProd (π β (π΄ β {π}) β¦ (πππ)))))) | ||
Theorem | dprd2da 19954* | 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 19955* | 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 19956* | 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 19957 | Lemma for dmdprdsplit 19959. (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 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 (π βΎ π·)) & β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) & β’ (π β ((πΊ DProd (π βΎ πΆ)) β© (πΊ DProd (π βΎ π·))) = { 0 }) β β’ (π β πΊdom DProd π) | ||
Theorem | dmdprdsplit 19959 | 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 19960 | 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 19961 | 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 19962 | 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 19963 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πΊ DProd (π βΎ {π})) = (πβπ)) | ||
Theorem | dpjcntz 19964 | The two subgroups that appear in dpjval 19968 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πΊ DProd (π βΎ (πΌ β {π}))))) | ||
Theorem | dpjdisj 19965 | The two subgroups that appear in dpjval 19968 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ 0 = (0gβπΊ) β β’ (π β ((πβπ) β© (πΊ DProd (π βΎ (πΌ β {π})))) = { 0 }) | ||
Theorem | dpjlsm 19966 | The two subgroups that appear in dpjval 19968 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ β = (LSSumβπΊ) β β’ (π β (πΊ DProd π) = ((πβπ) β (πΊ DProd (π βΎ (πΌ β {π}))))) | ||
Theorem | dpjfval 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 | dpjval 19968 | 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 19969 | 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 19970* | 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 19971* | 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 19972* | 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 19973 | 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 19974 | 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 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 πΊ)) | ||
Theorem | dpjghm2 19976 | 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 19977* | Lemma for ablfacrp2 19979. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΎ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ πΏ = {π₯ β π΅ β£ (πβπ₯) β₯ π} & β’ (π β πΊ β Abel) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π gcd π) = 1) & β’ (π β (β―βπ΅) = (π Β· π)) β β’ (π β ((β―βπΎ) gcd π) = 1) | ||
Theorem | ablfacrp 19978* | 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 19979* | The factors πΎ, πΏ of ablfacrp 19978 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 19980* | Lemma for ablfac1b 19982. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π = (πβ(π pCnt (β―βπ΅))) & β’ π = ((β―βπ΅) / π) β β’ ((π β§ π β π΄) β ((π β β β§ π β β) β§ (π gcd π) = 1 β§ (β―βπ΅) = (π Β· π))) | ||
Theorem | ablfac1a 19981* | The factors of ablfac1b 19982 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) β β’ ((π β§ π β π΄) β (β―β(πβπ)) = (πβ(π pCnt (β―βπ΅)))) | ||
Theorem | ablfac1b 19982* | 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 19983* | The factors of ablfac1b 19982 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π· = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ (π β π· β π΄) β β’ (π β (πΊ DProd π) = π΅) | ||
Theorem | ablfac1eulem 19984* | Lemma for ablfac1eu 19985. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ π = (π β π΄ β¦ {π₯ β π΅ β£ (πβπ₯) β₯ (πβ(π pCnt (β―βπ΅)))}) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β π΄ β β) & β’ π· = {π€ β β β£ π€ β₯ (β―βπ΅)} & β’ (π β π· β π΄) & β’ (π β (πΊdom DProd π β§ (πΊ DProd π) = π΅)) & β’ (π β dom π = π΄) & β’ ((π β§ π β π΄) β πΆ β β0) & β’ ((π β§ π β π΄) β (β―β(πβπ)) = (πβπΆ)) & β’ (π β π β β) & β’ (π β π΄ β Fin) β β’ (π β Β¬ π β₯ (β―β(πΊ DProd (π βΎ (π΄ β {π}))))) | ||
Theorem | ablfac1eu 19985* | The factorization of ablfac1b 19982 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 19986* | Lemma for pgpfac1 19992. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ πΎ = (mrClsβ(SubGrpβπΊ)) & β’ π = (πΎβ{π΄}) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΈ = (gExβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π pGrp πΊ) & β’ (π β πΊ β Abel) & β’ (π β π΅ β Fin) & β’ (π β (πβπ΄) = πΈ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π΄ β π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β (π β π) β π) & β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) β β’ ((π β§ πΆ β (π β (π β π))) β ((π β π) β (πΎβ{πΆ})) = π) | ||
Theorem | pgpfac1lem2 19987* | Lemma for pgpfac1 19992. (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 19988* | Lemma for pgpfac1 19992. (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 19989* | Lemma for pgpfac1 19992. (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 19990* | Lemma for pgpfac1 19992. (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 19991* | Lemma for pgpfac1 19992. (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 19992* | 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 19993* | Lemma for pgpfac 19996. (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 19994* | Lemma for pgpfac 19996. (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 19995* | Lemma for pgpfac 19996. (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 19996* | Full factorization of a finite abelian p-group, by iterating pgpfac1 19992. 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 19997* | Lemma for ablfac 20000. (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 19998* | Lemma for ablfac 20000. (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 19999* | Lemma for ablfac 20000. (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 20000* | 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 π ) = π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |