P. 241 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24001-24100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oppgtgp 24001	The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp)
Theorem	distgp 24002	Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵) → 𝐺 ∈ TopGrp)
Theorem	indistgp 24003	Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp)
Theorem	efmndtmd 24004	The monoid of endofunctions on a set 𝐴 is a topological monoid. Formerly part of proof for symgtgp 24009. (Contributed by AV, 23-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd)
Theorem	tmdlactcn 24005*	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 24006*	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 24007	A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd)
Theorem	subgtgp 24008	A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	symgtgp 24009	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 24010	A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 24012, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐽)
Theorem	opnsubg 24011	An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	clssubg 24012	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 24013	The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺))
Theorem	cldsubg 24014	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 24015*	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 24016*	The identity component, the connected component containing the identity element, is a closed (conncompcld 23337) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺))
Theorem	tgpconncompss 24017*	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 24018	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 24019	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 24020	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 24021	Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre))
Theorem	tgpt0 24022	Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2))
Theorem	qustgpopn 24023*	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 24024*	Lemma for qustgp 24025. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐾 = (TopOpen‘𝐻)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌))    &   ⊢ − = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌))    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	qustgp 24025	The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	qustgphaus 24026	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 24027	The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶TopMnd)    ⇒   ⊢ (𝜑 → 𝑌 ∈ TopMnd)
Theorem	prdstgpd 24028	The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶TopGrp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ TopGrp)
12.2.7  Infinite group sum on topological groups
Syntax	ctsu 24029	Extend class notation to include infinite group sums in a topological group.
class tsums
Definition	df-tsms 24030*	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 15612) and Σg (df-gsum 17364), 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 24031*	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 24032	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 24033*	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 24034*	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 24035	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 18651 etc. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))    &   ⊢ (𝜑 → (TopOpen‘𝐺) = (TopOpen‘𝐻))    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐻 tsums 𝐹))
Theorem	eltsms 24036*	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 24037*	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 24038	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 24039*	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 24040	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 24041	One half of tgptsmscls 24053, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹))
Theorem	tsmsgsum 24042	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 24043	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 24044	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 24045*	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 24046	Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopSp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆))
Theorem	tsmsres 24047	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 24048	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 24049	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 24050	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 24051	Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝐺 tsums (𝐼 ∘ 𝐹)))
Theorem	tsmssub 24052	The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻)))
Theorem	tgptsmscls 24053	A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 24013, 0nsg 19066. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋}))
Theorem	tgptsmscld 24054	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 24055	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 24056*	Lemma for tsmsxp 24058. (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 24057*	Lemma for tsmsxp 24058. (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 24058*	Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19873 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24056 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 𝐻))
12.2.8  Topological rings, fields, vector spaces
Syntax	ctrg 24059	The class of all topological division rings.
class TopRing
Syntax	ctdrg 24060	The class of all topological division rings.
class TopDRing
Syntax	ctlm 24061	The class of all topological modules.
class TopMod
Syntax	ctvc 24062	The class of all topological vector spaces.
class TopVec
Definition	df-trg 24063	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 24064	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 24065	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 24066	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 24067	Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopRing ↔ (𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd))
Theorem	trgtmd 24068	The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopRing → 𝑀 ∈ TopMnd)
Theorem	istdrg 24069	Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s 𝑈) ∈ TopGrp))
Theorem	tdrgunit 24070	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 24071	A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp)
Theorem	trgtmd2 24072	A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd)
Theorem	trgtps 24073	A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopSp)
Theorem	trgring 24074	A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Ring)
Theorem	trggrp 24075	A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Grp)
Theorem	tdrgtrg 24076	A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopRing)
Theorem	tdrgdrng 24077	A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ DivRing)
Theorem	tdrgring 24078	A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ Ring)
Theorem	tdrgtmd 24079	A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopMnd)
Theorem	tdrgtps 24080	A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopSp)
Theorem	istdrg2 24081	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 24082	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 24083	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 24084	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 24085*	Continuity of ring multiplication; analogue of cnmpt12f 23569 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 24086*	Continuity of ring multiplication; analogue of cnmpt22f 23578 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 24087	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 24088	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 24089	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 24090	A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd)
Theorem	tlmtps 24091	A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
Theorem	tlmlmod 24092	A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod)
Theorem	tlmtrg 24093	The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing)
Theorem	tlmscatps 24094	The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
Theorem	istvc 24095	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 24096	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 24097*	Continuity of scalar multiplication; analogue of cnmpt12f 23569 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 24098*	Continuity of scalar multiplication; analogue of cnmpt22f 23578 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 24099	A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)
Theorem	tvctlm 24100	A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod)