Home | Metamath
Proof Explorer Theorem List (p. 235 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tsmsfbas 23401* | 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 23402 | 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 23403* | 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 23404* | 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 23405 | 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 18516 etc. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ (π β (BaseβπΊ) = (Baseβπ»)) & β’ (π β (+gβπΊ) = (+gβπ»)) & β’ (π β (TopOpenβπΊ) = (TopOpenβπ»)) β β’ (π β (πΊ tsums πΉ) = (π» tsums πΉ)) | ||
Theorem | eltsms 23406* | 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 23407* | 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 23408 | 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 23409* | 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 23410 | 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 23411 | One half of tgptsmscls 23423, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β ((clsβπ½)β{π}) β (πΊ tsums πΉ)) | ||
Theorem | tsmsgsum 23412 | 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 23413 | 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 23414 | 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 23415* | 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 23416 | Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (π β π΄ β π) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopSp) & β’ (π β π β (SubMndβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ π» = (πΊ βΎs π) β β’ (π β (π» tsums πΉ) = ((πΊ tsums πΉ) β© π)) | ||
Theorem | tsmsres 23417 | 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 23418 | 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 23419 | 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 23420 | 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 23421 | Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ πΌ = (invgβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β (πΌβπ) β (πΊ tsums (πΌ β πΉ))) | ||
Theorem | tsmssub 23422 | The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π»:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) & β’ (π β π β (πΊ tsums π»)) β β’ (π β (π β π) β (πΊ tsums (πΉ βf β π»))) | ||
Theorem | tgptsmscls 23423 | A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 23383, 0nsg 18903. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopGrp) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π β (πΊ tsums πΉ)) β β’ (π β (πΊ tsums πΉ) = ((clsβπ½)β{π})) | ||
Theorem | tgptsmscld 23424 | 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 23425 | 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 23426* | Lemma for tsmsxp 23428. (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 23427* | Lemma for tsmsxp 23428. (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 23428* | Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19682 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 23426 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 23429 | The class of all topological division rings. |
class TopRing | ||
Syntax | ctdrg 23430 | The class of all topological division rings. |
class TopDRing | ||
Syntax | ctlm 23431 | The class of all topological modules. |
class TopMod | ||
Syntax | ctvc 23432 | The class of all topological vector spaces. |
class TopVec | ||
Definition | df-trg 23433 | 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 23434 | 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 23435 | 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 23436 | 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 23437 | Express the predicate "π is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) β β’ (π β TopRing β (π β TopGrp β§ π β Ring β§ π β TopMnd)) | ||
Theorem | trgtmd 23438 | The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) β β’ (π β TopRing β π β TopMnd) | ||
Theorem | istdrg 23439 | Express the predicate "π is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (mulGrpβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β (π β TopRing β§ π β DivRing β§ (π βΎs π) β TopGrp)) | ||
Theorem | tdrgunit 23440 | 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 23441 | A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopGrp) | ||
Theorem | trgtmd2 23442 | A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopMnd) | ||
Theorem | trgtps 23443 | A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β TopSp) | ||
Theorem | trgring 23444 | A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β Ring) | ||
Theorem | trggrp 23445 | A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopRing β π β Grp) | ||
Theorem | tdrgtrg 23446 | A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopRing) | ||
Theorem | tdrgdrng 23447 | A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β DivRing) | ||
Theorem | tdrgring 23448 | A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β Ring) | ||
Theorem | tdrgtmd 23449 | A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopMnd) | ||
Theorem | tdrgtps 23450 | A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopDRing β π β TopSp) | ||
Theorem | istdrg2 23451 | 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 23452 | 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 23453 | 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 23454 | 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 23455* | Continuity of ring multiplication; analogue of cnmpt12f 22939 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 23456* | Continuity of ring multiplication; analogue of cnmpt22f 22948 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 23457 | 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 23458 | 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 23459 | 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 23460 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopMnd) | ||
Theorem | tlmtps 23461 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopSp) | ||
Theorem | tlmlmod 23462 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β LMod) | ||
Theorem | tlmtrg 23463 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopRing) | ||
Theorem | tlmscatps 23464 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopSp) | ||
Theorem | istvc 23465 | 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 23466 | 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 23467* | Continuity of scalar multiplication; analogue of cnmpt12f 22939 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 23468* | Continuity of scalar multiplication; analogue of cnmpt22f 22948 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 23469 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopMod β π β TopGrp) | ||
Theorem | tvctlm 23470 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopVec β π β TopMod) | ||
Theorem | tvclmod 23471 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopVec β π β LMod) | ||
Theorem | tvclvec 23472 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β TopVec β π β LVec) | ||
Syntax | cust 23473 | Extend class notation with the class function of uniform structures. |
class UnifOn | ||
Definition | df-ust 23474* | Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.) |
β’ UnifOn = (π₯ β V β¦ {π’ β£ (π’ β π« (π₯ Γ π₯) β§ (π₯ Γ π₯) β π’ β§ βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) | ||
Theorem | ustfn 23475 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
β’ UnifOn Fn V | ||
Theorem | ustval 23476* | The class of all uniform structures for a base π. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
β’ (π β π β (UnifOnβπ) = {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) | ||
Theorem | isust 23477* | The predicate "π is a uniform structure with base π". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
β’ (π β π β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) | ||
Theorem | ustssxp 23478 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π Γ π)) | ||
Theorem | ustssel 23479 | A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.) |
β’ ((π β (UnifOnβπ) β§ π β π β§ π β (π Γ π)) β (π β π β π β π)) | ||
Theorem | ustbasel 23480 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
β’ (π β (UnifOnβπ) β (π Γ π) β π) | ||
Theorem | ustincl 23481 | A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β© π) β π) | ||
Theorem | ustdiag 23482 | The diagonal set is included in any entourage, i.e. any point is π -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π) β ( I βΎ π) β π) | ||
Theorem | ustinvel 23483 | If π is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π) β β‘π β π) | ||
Theorem | ustexhalf 23484* | For each entourage π there is an entourage π€ that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (π€ β π€) β π) | ||
Theorem | ustrel 23485 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) | ||
Theorem | ustfilxp 23486 | A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ ((π β β β§ π β (UnifOnβπ)) β π β (Filβ(π Γ π))) | ||
Theorem | ustne0 23487 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
β’ (π β (UnifOnβπ) β π β β ) | ||
Theorem | ustssco 23488 | In an uniform structure, any entourage π is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) | ||
Theorem | ustexsym 23489* | In an uniform structure, for any entourage π, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π)) | ||
Theorem | ustex2sym 23490* | In an uniform structure, for any entourage π, there exists a symmetrical entourage smaller than half π. (Contributed by Thierry Arnoux, 16-Jan-2018.) |
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β π€) β π)) | ||
Theorem | ustex3sym 23491* | In an uniform structure, for any entourage π, there exists a symmetrical entourage smaller than a third of π. (Contributed by Thierry Arnoux, 16-Jan-2018.) |
β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ (π€ β (π€ β π€)) β π)) | ||
Theorem | ustref 23492 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ππ΄) | ||
Theorem | ust0 23493 | The unique uniform structure of the empty set is the empty set. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
β’ (UnifOnββ ) = {{β }} | ||
Theorem | ustn0 23494 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
β’ Β¬ β β βͺ ran UnifOn | ||
Theorem | ustund 23495 | If two intersecting sets π΄ and π΅ are both small in π, their union is small in (πβ2). Proposition 1 of [BourbakiTop1] p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
β’ (π β (π΄ Γ π΄) β π) & β’ (π β (π΅ Γ π΅) β π) & β’ (π β (π΄ β© π΅) β β ) β β’ (π β ((π΄ βͺ π΅) Γ (π΄ βͺ π΅)) β (π β π)) | ||
Theorem | ustelimasn 23496 | Any point π΄ is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ β (π β {π΄})) | ||
Theorem | ustneism 23497 | For a point π΄ in π, (π β {π΄}) is small enough in (π β β‘π). This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
β’ ((π β (π Γ π) β§ π΄ β π) β ((π β {π΄}) Γ (π β {π΄})) β (π β β‘π)) | ||
Theorem | elrnustOLD 23498 | Obsolete version of elfvunirn 6870 as of 12-Jan-2025. (Contributed by Thierry Arnoux, 16-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β (UnifOnβπ) β π β βͺ ran UnifOn) | ||
Theorem | ustbas2 23499 | Second direction for ustbas 23501. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
β’ (π β (UnifOnβπ) β π = dom βͺ π) | ||
Theorem | ustuni 23500 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
β’ (π β (UnifOnβπ) β βͺ π = (π Γ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |