![]() |
Metamath
Proof Explorer Theorem List (p. 237 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oppgtgp 23601 | The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (πΊ β TopGrp β π β TopGrp) | ||
Theorem | distgp 23602 | Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β Grp β§ π½ = π« π΅) β πΊ β TopGrp) | ||
Theorem | indistgp 23603 | Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β Grp β§ π½ = {β , π΅}) β πΊ β TopGrp) | ||
Theorem | efmndtmd 23604 | The monoid of endofunctions on a set π΄ is a topological monoid. Formerly part of proof for symgtgp 23609. (Contributed by AV, 23-Feb-2024.) |
β’ π = (EndoFMndβπ΄) β β’ (π΄ β π β π β TopMnd) | ||
Theorem | tmdlactcn 23605* | The left group action of element π΄ in a topological monoid πΊ is a continuous function. (Contributed by FL, 18-Mar-2008.) (Revised by Mario Carneiro, 14-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ (π΄ + π₯)) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopMnd β§ π΄ β π) β πΉ β (π½ Cn π½)) | ||
Theorem | tgplacthmeo 23606* | The left group action of element π΄ in a topological group πΊ is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ (π΄ + π₯)) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π΄ β π) β πΉ β (π½Homeoπ½)) | ||
Theorem | submtmd 23607 | A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β TopMnd β§ π β (SubMndβπΊ)) β π» β TopMnd) | ||
Theorem | subgtgp 23608 | A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π» β TopGrp) | ||
Theorem | symgtgp 23609 | The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof shortened by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β πΊ β TopGrp) | ||
Theorem | subgntr 23610 | A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 23612, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π β π½) | ||
Theorem | opnsubg 23611 | An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π β π½) β π β (Clsdβπ½)) | ||
Theorem | clssubg 23612 | The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β (SubGrpβπΊ)) | ||
Theorem | clsnsg 23613 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β ((clsβπ½)βπ) β (NrmSGrpβπΊ)) | ||
Theorem | cldsubg 23614 | A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ π = (πΊ ~QG π) & β’ π = (BaseβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π ) β Fin) β (π β (Clsdβπ½) β π β π½)) | ||
Theorem | tgpconncompeqg 23615* | The connected component containing π΄ is the left coset of the identity component containing π΄. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} & β’ βΌ = (πΊ ~QG π) β β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) | ||
Theorem | tgpconncomp 23616* | The identity component, the connected component containing the identity element, is a closed (conncompcld 22937) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ (πΊ β TopGrp β π β (NrmSGrpβπΊ)) | ||
Theorem | tgpconncompss 23617* | The identity component is a subset of any open subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π β π½) β π β π) | ||
Theorem | ghmcnp 23618 | A group homomorphism on topological groups is continuous everywhere if it is continuous at any point. (Contributed by Mario Carneiro, 21-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») β β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β π β§ πΉ β (π½ Cn πΎ)))) | ||
Theorem | snclseqg 23619 | The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ 0 = (0gβπΊ) & β’ βΌ = (πΊ ~QG π) & β’ π = ((clsβπ½)β{ 0 }) β β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = ((clsβπ½)β{π΄})) | ||
Theorem | tgphaus 23620 | A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β { 0 } β (Clsdβπ½))) | ||
Theorem | tgpt1 23621 | Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β π½ β Fre)) | ||
Theorem | tgpt0 23622 | Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β π½ β Kol2)) | ||
Theorem | qustgpopn 23623* | A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») & β’ πΉ = (π₯ β π β¦ [π₯](πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β π½) β (πΉ β π) β πΎ) | ||
Theorem | qustgplem 23624* | Lemma for qustgp 23625. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») & β’ πΉ = (π₯ β π β¦ [π₯](πΊ ~QG π)) & β’ β = (π§ β π, π€ β π β¦ [(π§(-gβπΊ)π€)](πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β π» β TopGrp) | ||
Theorem | qustgp 23625 | The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β π» β TopGrp) | ||
Theorem | qustgphaus 23626 | The quotient of a topological group by a closed normal subgroup is a Hausdorff topological group. In particular, the quotient by the closure of the identity is a Hausdorff topological group, isomorphic to both the Kolmogorov quotient and the Hausdorff quotient operations on topological spaces (because T0 and Hausdorff coincide for topological groups). (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΎ β Haus) | ||
Theorem | prdstmdd 23627 | The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆTopMnd) β β’ (π β π β TopMnd) | ||
Theorem | prdstgpd 23628 | The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆTopGrp) β β’ (π β π β TopGrp) | ||
Syntax | ctsu 23629 | Extend class notation to include infinite group sums in a topological group. |
class tsums | ||
Definition | df-tsms 23630* | Define the set of limit points of an infinite group sum for the topological group πΊ. If πΊ is Hausdorff, then there will be at most one element in this set and βͺ (π tsums πΉ) selects this unique element if it exists. (π tsums πΉ) β 1o is a way to say that the sum exists and is unique. Note that unlike Ξ£ (df-sum 15632) and Ξ£g (df-gsum 17387), this does not return the sum itself, but rather the set of all such sums, which is usually either empty or a singleton. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ tsums = (π€ β V, π β V β¦ β¦(π« dom π β© Fin) / π β¦(((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦))))) | ||
Theorem | tsmsfbas 23631* | The collection of all sets of the form πΉ(π§) = {π¦ β π β£ π§ β π¦}, which can be read as the set of all finite subsets of π΄ which contain π§ as a subset, for each finite subset π§ of π΄, form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (π« π΄ β© Fin) & β’ πΉ = (π§ β π β¦ {π¦ β π β£ π§ β π¦}) & β’ πΏ = ran πΉ & β’ (π β π΄ β π) β β’ (π β πΏ β (fBasβπ)) | ||
Theorem | tsmslem1 23632 | The finite partial sums of a function πΉ are defined in a commutative monoid. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (π« π΄ β© Fin) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ ((π β§ π β π) β (πΊ Ξ£g (πΉ βΎ π)) β π΅) | ||
Theorem | tsmsval2 23633* | Definition of the topological group sum(s) of a collection πΉ(π₯) of values in the group with index set π΄. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (π« π΄ β© Fin) & β’ πΏ = ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) & β’ (π β πΊ β π) & β’ (π β πΉ β π) & β’ (π β dom πΉ = π΄) β β’ (π β (πΊ tsums πΉ) = ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) | ||
Theorem | tsmsval 23634* | Definition of the topological group sum(s) of a collection πΉ(π₯) of values in the group with index set π΄. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (π« π΄ β© Fin) & β’ πΏ = ran (π§ β π β¦ {π¦ β π β£ π§ β π¦}) & β’ (π β πΊ β π) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΊ tsums πΉ) = ((π½ fLimf (πfilGenπΏ))β(π¦ β π β¦ (πΊ Ξ£g (πΉ βΎ π¦))))) | ||
Theorem | tsmspropd 23635 | The group sum depends only on the base set, additive operation, and topology components. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd 18649 etc. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ (π β (BaseβπΊ) = (Baseβπ»)) & β’ (π β (+gβπΊ) = (+gβπ»)) & β’ (π β (TopOpenβπΊ) = (TopOpenβπ»)) β β’ (π β (πΊ tsums πΉ) = (π» tsums πΉ)) | ||
Theorem | eltsms 23636* | The property of being a sum of the sequence πΉ in the topological commutative monoid πΊ. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (π« π΄ β© Fin) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΆ β (πΊ tsums πΉ) β (πΆ β π΅ β§ βπ’ β π½ (πΆ β π’ β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π’))))) | ||
Theorem | tsmsi 23637* | The property of being a sum of the sequence πΉ in the topological commutative monoid πΊ. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (π« π΄ β© Fin) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΆ β (πΊ tsums πΉ)) & β’ (π β π β π½) & β’ (π β πΆ β π) β β’ (π β βπ§ β π βπ¦ β π (π§ β π¦ β (πΊ Ξ£g (πΉ βΎ π¦)) β π)) | ||
Theorem | tsmscl 23638 | A sum in a topological group is an element of the group. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΊ tsums πΉ) β π΅) | ||
Theorem | haustsms 23639* | In a Hausdorff topological group, a sum has at most one limit point. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ π½ = (TopOpenβπΊ) & β’ (π β π½ β Haus) β β’ (π β β*π₯ π₯ β (πΊ tsums πΉ)) | ||
Theorem | haustsms2 23640 | In a Hausdorff topological group, a sum has at most one limit point. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ π½ = (TopOpenβπΊ) & β’ (π β π½ β Haus) β β’ (π β (π β (πΊ tsums πΉ) β (πΊ tsums πΉ) = {π})) | ||
Theorem | tsmscls 23641 | One half of tgptsmscls 23653, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β ((clsβπ½)β{π}) β (πΊ tsums πΉ)) | ||
Theorem | tsmsgsum 23642 | The convergent points of a finite topological group sum are the closure of the finite group sum operation. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ π½ = (TopOpenβπΊ) β β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{(πΊ Ξ£g πΉ)})) | ||
Theorem | tsmsid 23643 | If a sum is finite, the usual sum is always a limit point of the topological sum (although it may not be the only limit point). (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g πΉ) β (πΊ tsums πΉ)) | ||
Theorem | haustsmsid 23644 | In a Hausdorff topological group, a finite sum sums to exactly the usual number with no extraneous limit points. By setting the topology to the discrete topology (which is Hausdorff), this theorem can be used to turn any tsums theorem into a Ξ£g theorem, so that the infinite group sum operation can be viewed as a generalization of the finite group sum. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) & β’ π½ = (TopOpenβπΊ) & β’ (π β π½ β Haus) β β’ (π β (πΊ tsums πΉ) = {(πΊ Ξ£g πΉ)}) | ||
Theorem | tsms0 23645* | The sum of zero is zero. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) β β’ (π β 0 β (πΊ tsums (π₯ β π΄ β¦ 0 ))) | ||
Theorem | tsmssubm 23646 | Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (π β π΄ β π) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π β (SubMndβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ π» = (πΊ βΎs π) β β’ (π β (π» tsums πΉ) = ((πΊ tsums πΉ) β© π)) | ||
Theorem | tsmsres 23647 | Extend an infinite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 18-Sep-2015.) (Revised by AV, 25-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp 0 ) β π) β β’ (π β (πΊ tsums (πΉ βΎ π)) = (πΊ tsums πΉ)) | ||
Theorem | tsmsf1o 23648 | Re-index an infinite group sum using a bijection. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:πΆβ1-1-ontoβπ΄) β β’ (π β (πΊ tsums πΉ) = (πΊ tsums (πΉ β π»))) | ||
Theorem | tsmsmhm 23649 | Apply a continuous group homomorphism to an infinite group sum. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π» β CMnd) & β’ (π β π» β TopSp) & β’ (π β πΆ β (πΊ MndHom π»)) & β’ (π β πΆ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β (πΆβπ) β (π» tsums (πΆ β πΉ))) | ||
Theorem | tsmsadd 23650 | The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) & β’ (π β π β (πΊ tsums π»)) β β’ (π β (π + π) β (πΊ tsums (πΉ βf + π»))) | ||
Theorem | tsmsinv 23651 | Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ πΌ = (invgβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β (πΌβπ) β (πΊ tsums (πΌ β πΉ))) | ||
Theorem | tsmssub 23652 | The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) & β’ (π β π β (πΊ tsums π»)) β β’ (π β (π β π) β (πΊ tsums (πΉ βf β π»))) | ||
Theorem | tgptsmscls 23653 | A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 23613, 0nsg 19048. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{π})) | ||
Theorem | tgptsmscld 23654 | The set of limit points to an infinite sum in a topological group is closed. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΊ tsums πΉ) β (Clsdβπ½)) | ||
Theorem | tsmssplit 23655 | Split a topological group sum into two parts. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums (πΉ βΎ πΆ))) & β’ (π β π β (πΊ tsums (πΉ βΎ π·))) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (π + π) β (πΊ tsums πΉ)) | ||
Theorem | tsmsxplem1 23656* | Lemma for tsmsxp 23658. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ ((π β§ π β π΄) β (π»βπ) β (πΊ tsums (π β πΆ β¦ (ππΉπ)))) & β’ π½ = (TopOpenβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΏ β π½) & β’ (π β 0 β πΏ) & β’ (π β πΎ β (π« π΄ β© Fin)) & β’ (π β dom π· β πΎ) & β’ (π β π· β (π« (π΄ Γ πΆ) β© Fin)) β β’ (π β βπ β (π« πΆ β© Fin)(ran π· β π β§ βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ)) | ||
Theorem | tsmsxplem2 23657* | Lemma for tsmsxp 23658. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ ((π β§ π β π΄) β (π»βπ) β (πΊ tsums (π β πΆ β¦ (ππΉπ)))) & β’ π½ = (TopOpenβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΏ β π½) & β’ (π β 0 β πΏ) & β’ (π β πΎ β (π« π΄ β© Fin)) & β’ (π β βπ β π βπ β π (π + π) β π) & β’ (π β π β (π« πΆ β© Fin)) & β’ (π β π· β (πΎ Γ π)) & β’ (π β βπ₯ β πΎ ((π»βπ₯) β (πΊ Ξ£g (πΉ βΎ ({π₯} Γ π)))) β πΏ) & β’ (π β (πΊ Ξ£g (πΉ βΎ (πΎ Γ π))) β π) & β’ (π β βπ β (πΏ βm πΎ)(πΊ Ξ£g π) β π) β β’ (π β (πΊ Ξ£g (π» βΎ πΎ)) β π) | ||
Theorem | tsmsxp 23658* | Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19843 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 23656 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β πΉ:(π΄ Γ πΆ)βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ ((π β§ π β π΄) β (π»βπ) β (πΊ tsums (π β πΆ β¦ (ππΉπ)))) β β’ (π β (πΊ tsums πΉ) β (πΊ tsums π»)) | ||
Syntax | ctrg 23659 | The class of all topological division rings. |
class TopRing | ||
Syntax | ctdrg 23660 | The class of all topological division rings. |
class TopDRing | ||
Syntax | ctlm 23661 | The class of all topological modules. |
class TopMod | ||
Syntax | ctvc 23662 | The class of all topological vector spaces. |
class TopVec | ||
Definition | df-trg 23663 | Define a topological ring, which is a ring such that the addition is a topological group operation and the multiplication is continuous. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ TopRing = {π β (TopGrp β© Ring) β£ (mulGrpβπ) β TopMnd} | ||
Definition | df-tdrg 23664 | Define a topological division ring (which differs from a topological field only in being potentially noncommutative), which is a division ring and topological ring such that the unit group of the division ring (which is the set of nonzero elements) is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ TopDRing = {π β (TopRing β© DivRing) β£ ((mulGrpβπ) βΎs (Unitβπ)) β TopGrp} | ||
Definition | df-tlm 23665 | Define a topological left module, which is just what its name suggests: instead of a group over a ring with a scalar product connecting them, it is a topological group over a topological ring with a continuous scalar product. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ TopMod = {π€ β (TopMnd β© LMod) β£ ((Scalarβπ€) β TopRing β§ ( Β·sf βπ€) β (((TopOpenβ(Scalarβπ€)) Γt (TopOpenβπ€)) Cn (TopOpenβπ€)))} | ||
Definition | df-tvc 23666 | Define a topological left vector space, which is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ TopVec = {π€ β TopMod β£ (Scalarβπ€) β TopDRing} | ||
Theorem | istrg 23667 | Express the predicate "π is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) β β’ (π β TopRing β (π β TopGrp β§ π β Ring β§ π β TopMnd)) | ||
Theorem | trgtmd 23668 | The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) β β’ (π β TopRing β π β TopMnd) | ||
Theorem | istdrg 23669 | Express the predicate "π is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β (π β TopRing β§ π β DivRing β§ (π βΎs π) β TopGrp)) | ||
Theorem | tdrgunit 23670 | The unit group of a topological division ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β (π βΎs π) β TopGrp) | ||
Theorem | trgtgp 23671 | A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopGrp) | ||
Theorem | trgtmd2 23672 | A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopMnd) | ||
Theorem | trgtps 23673 | A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopSp) | ||
Theorem | trgring 23674 | A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β Ring) | ||
Theorem | trggrp 23675 | A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β Grp) | ||
Theorem | tdrgtrg 23676 | A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopRing) | ||
Theorem | tdrgdrng 23677 | A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β DivRing) | ||
Theorem | tdrgring 23678 | A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β Ring) | ||
Theorem | tdrgtmd 23679 | A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopMnd) | ||
Theorem | tdrgtps 23680 | A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopSp) | ||
Theorem | istdrg2 23681 | A topological-ring division ring is a topological division ring iff the group of nonzero elements is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β TopDRing β (π β TopRing β§ π β DivRing β§ (π βΎs (π΅ β { 0 })) β TopGrp)) | ||
Theorem | mulrcn 23682 | The functionalization of the ring multiplication operation is a continuous function in a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ π = (+πβ(mulGrpβπ )) β β’ (π β TopRing β π β ((π½ Γt π½) Cn π½)) | ||
Theorem | invrcn2 23683 | The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to itself. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ πΌ = (invrβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β πΌ β ((π½ βΎt π) Cn (π½ βΎt π))) | ||
Theorem | invrcn 23684 | The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to the field. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ πΌ = (invrβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β πΌ β ((π½ βΎt π) Cn π½)) | ||
Theorem | cnmpt1mulr 23685* | Continuity of ring multiplication; analogue of cnmpt12f 23169 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β TopRing) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn π½)) & β’ (π β (π₯ β π β¦ π΅) β (πΎ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πΎ Cn π½)) | ||
Theorem | cnmpt2mulr 23686* | Continuity of ring multiplication; analogue of cnmpt22f 23178 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β TopRing) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ Β· π΅)) β ((πΎ Γt πΏ) Cn π½)) | ||
Theorem | dvrcn 23687 | The division function is continuous in a topological field. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π½ = (TopOpenβπ ) & β’ / = (/rβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β / β ((π½ Γt (π½ βΎt π)) Cn π½)) | ||
Theorem | istlm 23688 | The predicate "π is a topological left module". (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β TopMod β ((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β§ Β· β ((πΎ Γt π½) Cn π½))) | ||
Theorem | vscacn 23689 | The scalar multiplication is continuous in a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β TopMod β Β· β ((πΎ Γt π½) Cn π½)) | ||
Theorem | tlmtmd 23690 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopMnd) | ||
Theorem | tlmtps 23691 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopSp) | ||
Theorem | tlmlmod 23692 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β LMod) | ||
Theorem | tlmtrg 23693 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopRing) | ||
Theorem | tlmscatps 23694 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopSp) | ||
Theorem | istvc 23695 | A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopVec β (π β TopMod β§ πΉ β TopDRing)) | ||
Theorem | tvctdrg 23696 | The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopVec β πΉ β TopDRing) | ||
Theorem | cnmpt1vsca 23697* | Continuity of scalar multiplication; analogue of cnmpt12f 23169 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) & β’ (π β π β TopMod) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΏ Cn πΎ)) & β’ (π β (π₯ β π β¦ π΅) β (πΏ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πΏ Cn π½)) | ||
Theorem | cnmpt2vsca 23698* | Continuity of scalar multiplication; analogue of cnmpt22f 23178 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) & β’ (π β π β TopMod) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΏ Γt π) Cn πΎ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΏ Γt π) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ Β· π΅)) β ((πΏ Γt π) Cn π½)) | ||
Theorem | tlmtgp 23699 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopGrp) | ||
Theorem | tvctlm 23700 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopVec β π β TopMod) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |