![]() |
Metamath
Proof Explorer Theorem List (p. 200 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gsumpr 19901* | Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π = π β π΄ = πΆ) & β’ (π = π β π΄ = π·) β β’ ((πΊ β CMnd β§ (π β π β§ π β π β§ π β π) β§ (πΆ β π΅ β§ π· β π΅)) β (πΊ Ξ£g (π β {π, π} β¦ π΄)) = (πΆ + π·)) | ||
Theorem | gsumzunsnd 19902* | Append an element to a finite group sum, more general version of gsumunsnd 19904. (Contributed by AV, 7-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π = (CntzβπΊ) & β’ πΉ = (π β (π΄ βͺ {π}) β¦ π) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β Fin) & β’ (π β ran πΉ β (πβran πΉ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnfd 19903* | Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) & β’ β²ππ β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnd 19904* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 2-Jan-2019.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsnf 19905* | Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ (π = π β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumunsn 19906* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Proof shortened by AV, 8-Mar-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π) & β’ (π β Β¬ π β π΄) & β’ (π β π β π΅) & β’ (π = π β π = π) β β’ (π β (πΊ Ξ£g (π β (π΄ βͺ {π}) β¦ π)) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) | ||
Theorem | gsumdifsnd 19907* | Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β (π β π΄ β¦ π) finSupp (0gβπΊ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β (π΄ β {π}) β¦ π)) + π)) | ||
Theorem | gsumpt 19908 | Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp 0 ) β {π}) β β’ (π β (πΊ Ξ£g πΉ) = (πΉβπ)) | ||
Theorem | gsummptf1o 19909* | Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.) |
β’ β²π₯π» & β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π₯ = πΈ β πΆ = π») & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΉ β π΅) & β’ ((π β§ π₯ β π΄) β πΆ β πΉ) & β’ ((π β§ π¦ β π·) β πΈ β π΄) & β’ ((π β§ π₯ β π΄) β β!π¦ β π· π₯ = πΈ) β β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ πΆ)) = (πΊ Ξ£g (π¦ β π· β¦ π»))) | ||
Theorem | gsummptun 19910* | Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β CMnd) & β’ (π β (π΄ βͺ πΆ) β Fin) & β’ (π β (π΄ β© πΆ) = β ) & β’ ((π β§ π₯ β (π΄ βͺ πΆ)) β π· β π΅) β β’ (π β (π Ξ£g (π₯ β (π΄ βͺ πΆ) β¦ π·)) = ((π Ξ£g (π₯ β π΄ β¦ π·)) + (π Ξ£g (π₯ β πΆ β¦ π·)))) | ||
Theorem | gsummpt1n0 19911* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 19912. (Contributed by AV, 11-Oct-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ πΉ = (π β πΌ β¦ if(π = π, π΄, 0 )) & β’ (π β βπ β πΌ π΄ β (BaseβπΊ)) β β’ (π β (πΊ Ξ£g πΉ) = β¦π / πβ¦π΄) | ||
Theorem | gsummptif1n0 19912* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019.) (Proof shortened by AV, 11-Oct-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ πΉ = (π β πΌ β¦ if(π = π, π΄, 0 )) & β’ (π β π΄ β (BaseβπΊ)) β β’ (π β (πΊ Ξ£g πΉ) = π΄) | ||
Theorem | gsummptcl 19913* | Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β Fin) & β’ (π β βπ β π π β π΅) β β’ (π β (πΊ Ξ£g (π β π β¦ π)) β π΅) | ||
Theorem | gsummptfif1o 19914* | Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π β Fin) & β’ (π β βπ β π π β π΅) & β’ πΉ = (π β π β¦ π) & β’ (π β π»:πΆβ1-1-ontoβπ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) | ||
Theorem | gsummptfzcl 19915* | Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΌ = (π...π)) & β’ (π β βπ β πΌ π β π΅) β β’ (π β (πΊ Ξ£g (π β πΌ β¦ π)) β π΅) | ||
Theorem | gsum2dlem1 19916* | Lemma 1 for gsum2d 19918. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ))) β π΅) | ||
Theorem | gsum2dlem2 19917* | Lemma for gsum2d 19918. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βΎ (π΄ βΎ dom (πΉ supp 0 )))) = (πΊ Ξ£g (π β dom (πΉ supp 0 ) β¦ (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ)))))) | ||
Theorem | gsum2d 19918* | Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β Rel π΄) & β’ (π β π· β π) & β’ (π β dom π΄ β π·) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β π· β¦ (πΊ Ξ£g (π β (π΄ β {π}) β¦ (ππΉπ)))))) | ||
Theorem | gsum2d2lem 19919* | Lemma for gsum2d2 19920: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (π β π΄, π β πΆ β¦ π) finSupp 0 ) | ||
Theorem | gsum2d2 19920* | Write a group sum over a two-dimensional region as a double sum. Note that πΆ(π) is a function of π. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π))))) | ||
Theorem | gsumcom2 19921* | Two-dimensional commutation of a group sum. Note that while π΄ and π· are constants w.r.t. π, π, πΆ(π) and πΈ(π) are not. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) & β’ (π β π· β π) & β’ (π β ((π β π΄ β§ π β πΆ) β (π β π· β§ π β πΈ))) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β π·, π β πΈ β¦ π))) | ||
Theorem | gsumxp 19922* | Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ (ππΉπ)))))) | ||
Theorem | gsumcom 19923* | Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄, π β πΆ β¦ π)) = (πΊ Ξ£g (π β πΆ, π β π΄ β¦ π))) | ||
Theorem | gsumcom3 19924* | A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) & β’ (π β π β Fin) & β’ ((π β§ ((π β π΄ β§ π β πΆ) β§ Β¬ πππ)) β π = 0 ) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π)))) = (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ π))))) | ||
Theorem | gsumcom3fi 19925* | A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΆ β Fin) & β’ ((π β§ (π β π΄ β§ π β πΆ)) β π β π΅) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ π)))) = (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ π))))) | ||
Theorem | gsumxp2 19926* | Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (π β πΆ β¦ (πΊ Ξ£g (π β π΄ β¦ (ππΉπ))))) = (πΊ Ξ£g (π β π΄ β¦ (πΊ Ξ£g (π β πΆ β¦ (ππΉπ)))))) | ||
Theorem | prdsgsum 19927* | Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β π) & β’ ((π β§ π₯ β πΌ) β π β CMnd) & β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β π΅) & β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) β β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π Ξ£g (π¦ β π½ β¦ π)))) | ||
Theorem | pwsgsum 19928* | Finite commutative sums in a power structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β CMnd) & β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β π΅) & β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) β β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π Ξ£g (π¦ β π½ β¦ π)))) | ||
Theorem | fsfnn0gsumfsffz 19929* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β π β β0) & β’ π» = (πΉ βΎ (0...π)) β β’ (π β (βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 ) β (πΊ Ξ£g πΉ) = (πΊ Ξ£g π»))) | ||
Theorem | nn0gsumfz 19930* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β πΉ finSupp 0 ) β β’ (π β βπ β β0 βπ β (π΅ βm (0...π ))(π = (πΉ βΎ (0...π )) β§ βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 ) β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) | ||
Theorem | nn0gsumfz0 19931* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β πΉ finSupp 0 ) β β’ (π β βπ β β0 βπ β (π΅ βm (0...π ))(πΊ Ξ£g πΉ) = (πΊ Ξ£g π)) | ||
Theorem | gsummptnn0fz 19932* | A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 3-Jul-2022.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β βπ β β0 πΆ β π΅) & β’ (π β π β β0) & β’ (π β βπ β β0 (π < π β πΆ = 0 )) β β’ (π β (πΊ Ξ£g (π β β0 β¦ πΆ)) = (πΊ Ξ£g (π β (0...π) β¦ πΆ))) | ||
Theorem | gsummptnn0fzfv 19933* | A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΉ β (π΅ βm β0)) & β’ (π β π β β0) & β’ (π β βπ₯ β β0 (π < π₯ β (πΉβπ₯) = 0 )) β β’ (π β (πΊ Ξ£g (π β β0 β¦ (πΉβπ))) = (πΊ Ξ£g (π β (0...π) β¦ (πΉβπ)))) | ||
Theorem | telgsumfzslem 19934* | Lemma for telgsumfzs 19935 (induction step). (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) β β’ ((π¦ β (β€β₯βπ) β§ (π β§ βπ β (π...((π¦ + 1) + 1))πΆ β π΅)) β ((πΊ Ξ£g (π β (π...π¦) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦(π¦ + 1) / πβ¦πΆ) β (πΊ Ξ£g (π β (π...(π¦ + 1)) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦((π¦ + 1) + 1) / πβ¦πΆ))) | ||
Theorem | telgsumfzs 19935* | Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β (β€β₯βπ)) & β’ (π β βπ β (π...(π + 1))πΆ β π΅) β β’ (π β (πΊ Ξ£g (π β (π...π) β¦ (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ))) = (β¦π / πβ¦πΆ β β¦(π + 1) / πβ¦πΆ)) | ||
Theorem | telgsumfz 19936* | Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15774. (Contributed by AV, 23-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β (β€β₯βπ)) & β’ (π β βπ β (π...(π + 1))π΄ β π΅) & β’ (π = π β π΄ = πΏ) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (π...π) β¦ (πΏ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsumfz0s 19937* | 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 19938* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15774. (Contributed by AV, 23-Nov-2019.) |
β’ πΎ = (BaseβπΊ) & β’ (π β πΊ β Abel) & β’ β = (-gβπΊ) & β’ (π β π β β0) & β’ (π β βπ β (0...(π + 1))π΄ β πΎ) & β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = 0 β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) β β’ (π β (πΊ Ξ£g (π β (0...π) β¦ (π΅ β πΆ))) = (π· β πΈ)) | ||
Theorem | telgsums 19939* | 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 19940* | 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 19941 | Internal direct product of a family of subgroups. |
class DProd | ||
Syntax | cdpj 19942 | Projection operator for a direct product. |
class dProj | ||
Definition | df-dprd 19943* | 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 19944* | 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 19945 | 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 19946* | 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 19947* | 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 19948 | 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 19949 | 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 19950 | 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 19951* | 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 19952* | 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 19953 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β πΊ β Grp) | ||
Theorem | dprdf 19954 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (πΊdom DProd π β π:dom πβΆ(SubGrpβπΊ)) | ||
Theorem | dprdf2 19955 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) β β’ (π β π:πΌβΆ(SubGrpβπΊ)) | ||
Theorem | dprdcntz 19956 | The function π is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πβπ))) | ||
Theorem | dprddisj 19957 | 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 19958* | 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 19959* | 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 19960* | 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 19961* | 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 19962* | 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 19963* | 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 19964 | 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 19965* | 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 19966* | 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 19967* | 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 19968* | 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 19969* | 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 19970* | 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 19971* | 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 19972 | 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 19973 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πβπ) β (πΊ DProd π)) | ||
Theorem | dprdlub 19974* | 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 19975 | 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 19976 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π΄ β πΌ) β β’ (π β (πΊdom DProd (π βΎ π΄) β§ (πΊ DProd (π βΎ π΄)) β (πΊ DProd π))) | ||
Theorem | dprdss 19977* | 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 19978* | 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 19979 | 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 19980 | 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 19981 | 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 19982 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) β β’ (π΄ β (SubGrpβπΊ) β (π»dom DProd π β (πΊdom DProd π β§ ran π β π« π΄))) | ||
Theorem | subgdprd 19983 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π» = (πΊ βΎs π΄) & β’ (π β π΄ β (SubGrpβπΊ)) & β’ (π β πΊdom DProd π) & β’ (π β ran π β π« π΄) β β’ (π β (π» DProd π) = (πΊ DProd π)) | ||
Theorem | dprdsn 19984 | 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 19985* | Lemma for dmdprdsplit 19995. (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 19986 | The function π is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β πΆ β πΌ) & β’ (π β π· β πΌ) & β’ (π β (πΆ β© π·) = β ) & β’ π = (CntzβπΊ) β β’ (π β (πΊ DProd (π βΎ πΆ)) β (πβ(πΊ DProd (π βΎ π·)))) | ||
Theorem | dprddisj2 19987 | 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 19988* | 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 19989* | 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 19990* | 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 19991* | 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 19992* | 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 19993 | Lemma for dmdprdsplit 19995. (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 19994 | 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 19995 | 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 19996 | 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 19997 | 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 19998 | 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 19999 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) β β’ (π β (πΊ DProd (π βΎ {π})) = (πβπ)) | ||
Theorem | dpjcntz 20000 | The two subgroups that appear in dpjval 20004 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
β’ (π β πΊdom DProd π) & β’ (π β dom π = πΌ) & β’ (π β π β πΌ) & β’ π = (CntzβπΊ) β β’ (π β (πβπ) β (πβ(πΊ DProd (π βΎ (πΌ β {π}))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |