Home | Metamath
Proof Explorer Theorem List (p. 227 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnextrel 22601 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹)) | ||
Theorem | cnextfun 22602 | 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 22603* | 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 22604* | 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 22605* | 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 22606* | 𝐹 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 22607 | 𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
Syntax | ctmd 22608 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 22609 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 22610* | 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 22611* | 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 22612 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐹 = (+𝑓‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | ||
Theorem | tmdmnd 22613 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | ||
Theorem | tmdtps 22614 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) | ||
Theorem | istgp 22615 | 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 22616 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | ||
Theorem | tgptmd 22617 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | ||
Theorem | tgptps 22618 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) | ||
Theorem | tmdtopon 22619 | 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 22620 | 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 22621 | 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 22622 | 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 22623 | 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 22624 | 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 22625* | Continuity of the group sum; analogue of cnmpt12f 22204 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 22626* | Continuity of the group sum; analogue of cnmpt22f 22213 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 22627* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | ||
Theorem | tgpsubcn 22628 | 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 22629 | 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 22630* | 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 22631* | 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 22632 | 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 23353 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 22633* | 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 22634* | 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 22635 | The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd) | ||
Theorem | oppgtgp 22636 | The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp) | ||
Theorem | distgp 22637 | Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵) → 𝐺 ∈ TopGrp) | ||
Theorem | indistgp 22638 | Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp) | ||
Theorem | symgtgp 22639 | The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp) | ||
Theorem | tmdlactcn 22640* | 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 22641* | 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 22642 | A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) | ||
Theorem | subgtgp 22643 | A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | subgntr 22644 | A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 22646, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐽) | ||
Theorem | opnsubg 22645 | An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | clssubg 22646 | 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 22647 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺)) | ||
Theorem | cldsubg 22648 | 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 22649* | 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 22650* | The identity component, the connected component containing the identity element, is a closed (conncompcld 21972) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | tgpconncompss 22651* | 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 22652 | 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 22653 | 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 22654 | 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 22655 | Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre)) | ||
Theorem | tgpt0 22656 | Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2)) | ||
Theorem | qustgpopn 22657* | 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 22658* | Lemma for qustgp 22659. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐾 = (TopOpen‘𝐻) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) & ⊢ − = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgp 22659 | The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgphaus 22660 | 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 22661 | The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopMnd) | ||
Theorem | prdstgpd 22662 | The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopGrp) | ||
Syntax | ctsu 22663 | Extend class notation to include infinite group sums in a topological group. |
class tsums | ||
Definition | df-tsms 22664* | 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 15033) and Σg (df-gsum 16706), 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 22665* | 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 22666 | 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 22667* | 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 22668* | 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 22669 | 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 17926 etc. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) & ⊢ (𝜑 → (TopOpen‘𝐺) = (TopOpen‘𝐻)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐻 tsums 𝐹)) | ||
Theorem | eltsms 22670* | 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 22671* | 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 22672 | 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 22673* | 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 22674 | 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 22675 | One half of tgptsmscls 22687, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) | ||
Theorem | tsmsgsum 22676 | 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 22677 | 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 22678 | 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 22679* | 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 22680 | Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆)) | ||
Theorem | tsmsres 22681 | 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 22682 | 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 22683 | 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 22684 | 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 22685 | Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝐺 tsums (𝐼 ∘ 𝐹))) | ||
Theorem | tsmssub 22686 | The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻)) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻))) | ||
Theorem | tgptsmscls 22687 | A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 22647, 0nsg 18261. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) | ||
Theorem | tgptsmscld 22688 | 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 22689 | 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 22690* | Lemma for tsmsxp 22692. (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 22691* | Lemma for tsmsxp 22692. (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 22692* | Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19027 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 22690 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 22693 | The class of all topological division rings. |
class TopRing | ||
Syntax | ctdrg 22694 | The class of all topological division rings. |
class TopDRing | ||
Syntax | ctlm 22695 | The class of all topological modules. |
class TopMod | ||
Syntax | ctvc 22696 | The class of all topological vector spaces. |
class TopVec | ||
Definition | df-trg 22697 | 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 22698 | 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 22699 | 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 22700 | 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} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |