P. 243 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24201-24300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnextrel 24201	In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹))
Theorem	cnextfun 24202	If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹))
Theorem	cnextfvval 24203*	The value of the continuous extension of a given function 𝐹 at a point 𝑋. (Contributed by Thierry Arnoux, 21-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))
Theorem	cnextf 24204*	Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
Theorem	cnextcn 24205*	Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology 𝐽 on 𝐶, a subset 𝐴 dense in 𝐶, this states a condition for 𝐹 from 𝐴 to a regular space 𝐾 to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ Reg)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	cnextfres1 24206*	𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 17-Jan-2018.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ Reg)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    ⇒   ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) = 𝐹)
Theorem	cnextfres 24207	𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋))
12.2.6  Topological groups
Syntax	ctmd 24208	Extend class notation with the class of all topological monoids.
class TopMnd
Syntax	ctgp 24209	Extend class notation with the class of all topological groups.
class TopGrp
Definition	df-tmd 24210*	Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ TopMnd = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)}
Definition	df-tgp 24211*	Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.)
⊢ TopGrp = {𝑓 ∈ (Grp ∩ TopMnd) ∣ [(TopOpen‘𝑓) / 𝑗](invg‘𝑓) ∈ (𝑗 Cn 𝑗)}
Theorem	istmd 24212	The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐹 = (+𝑓‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
Theorem	tmdmnd 24213	A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
Theorem	tmdtps 24214	A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp)
Theorem	istgp 24215	The predicate "is a topological group". Definition 1 of [BourbakiTop1] p. III.1. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ (𝐽 Cn 𝐽)))
Theorem	tgpgrp 24216	A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
Theorem	tgptmd 24217	A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
Theorem	tgptps 24218	A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
Theorem	tmdtopon 24219	The topology of a topological monoid. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
Theorem	tgptopon 24220	The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
Theorem	tmdcn 24221	In a topological monoid, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	tgpcn 24222	In a topological group, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	tgpinv 24223	In a topological group, the inverse function is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by FL, 27-Jun-2014.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐼 ∈ (𝐽 Cn 𝐽))
Theorem	grpinvhmeo 24224	The inverse function in a topological group is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐼 ∈ (𝐽Homeo𝐽))
Theorem	cnmpt1plusg 24225*	Continuity of the group sum; analogue of cnmpt12f 23804 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TopMnd)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝐾 Cn 𝐽))
Theorem	cnmpt2plusg 24226*	Continuity of the group sum; analogue of cnmpt22f 23813 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TopMnd)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 + 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
Theorem	tmdcn2 24227*	Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈))
Theorem	tgpsubcn 24228	In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of [BourbakiTop1] p. III.1. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	istgp2 24229	A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
Theorem	tmdmulg 24230*	In a topological monoid, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))
Theorem	tgpmulg 24231*	In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽))
Theorem	tgpmulg2 24232	In a topological monoid, the group multiple function is jointly continuous (although this is not saying much as one of the factors is discrete). Use zdis 24955 to write the left topology as a subset of the complex numbers. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → · ∈ ((𝒫 ℤ ×t 𝐽) Cn 𝐽))
Theorem	tmdgsum 24233*	In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when 𝐴 is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
Theorem	tmdgsum2 24234*	For any neighborhood 𝑈 of 𝑛𝑋, there is a neighborhood 𝑢 of 𝑋 such that any sum of 𝑛 elements in 𝑢 sums to an element of 𝑈. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopMnd)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
Theorem	oppgtmd 24235	The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd)
Theorem	oppgtgp 24236	The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp)
Theorem	distgp 24237	Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵) → 𝐺 ∈ TopGrp)
Theorem	indistgp 24238	Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp)
Theorem	efmndtmd 24239	The monoid of endofunctions on a set 𝐴 is a topological monoid. Formerly part of proof for symgtgp 24244. (Contributed by AV, 23-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd)
Theorem	tmdlactcn 24240*	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 24241*	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 24242	A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd)
Theorem	subgtgp 24243	A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	symgtgp 24244	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 24245	A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 24247, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐽)
Theorem	opnsubg 24246	An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	clssubg 24247	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 24248	The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺))
Theorem	cldsubg 24249	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 24250*	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 24251*	The identity component, the connected component containing the identity element, is a closed (conncompcld 23572) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺))
Theorem	tgpconncompss 24252*	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 24253	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 24254	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 24255	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 24256	Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre))
Theorem	tgpt0 24257	Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2))
Theorem	qustgpopn 24258*	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 24259*	Lemma for qustgp 24260. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐾 = (TopOpen‘𝐻)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌))    &   ⊢ − = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌))    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	qustgp 24260	The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))    ⇒   ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp)
Theorem	qustgphaus 24261	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 24262	The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶TopMnd)    ⇒   ⊢ (𝜑 → 𝑌 ∈ TopMnd)
Theorem	prdstgpd 24263	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 24264	Extend class notation to include infinite group sums in a topological group.
class tsums
Definition	df-tsms 24265*	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 15740) and Σg (df-gsum 17496), 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 24266*	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 24267	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 24268*	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 24269*	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 24270	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 18818 etc. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))    &   ⊢ (𝜑 → (TopOpen‘𝐺) = (TopOpen‘𝐻))    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐻 tsums 𝐹))
Theorem	eltsms 24271*	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 24272*	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 24273	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 24274*	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 24275	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 24276	One half of tgptsmscls 24288, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹))
Theorem	tsmsgsum 24277	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 24278	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 24279	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 24280*	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 24281	Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopSp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆))
Theorem	tsmsres 24282	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 24283	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 24284	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 24285	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 24286	Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝐺 tsums (𝐼 ∘ 𝐹)))
Theorem	tsmssub 24287	The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻))    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻)))
Theorem	tgptsmscls 24288	A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 24248, 0nsg 19236. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐺 ∈ TopGrp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹))    ⇒   ⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋}))
Theorem	tgptsmscld 24289	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 24290	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 24291*	Lemma for tsmsxp 24293. (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 24292*	Lemma for tsmsxp 24293. (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 24293*	Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 20047 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24291 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 24294	The class of all topological division rings.
class TopRing
Syntax	ctdrg 24295	The class of all topological division rings.
class TopDRing
Syntax	ctlm 24296	The class of all topological modules.
class TopMod
Syntax	ctvc 24297	The class of all topological vector spaces.
class TopVec
Definition	df-trg 24298	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 24299	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 24300	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‘𝑤)))}