Home | Metamath
Proof Explorer Theorem List (p. 228 of 450) | < 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-28691) |
Hilbert Space Explorer
(28692-30214) |
Users' Mathboxes
(30215-44982) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | indistgp 22701 | Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp) | ||
Theorem | efmndtmd 22702 | The monoid of endofunctions on a set 𝐴 is a topological monoid. Formerly part of proof for symgtgp 22707. (Contributed by AV, 23-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd) | ||
Theorem | tmdlactcn 22703* | 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 22704* | 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 22705 | A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) | ||
Theorem | subgtgp 22706 | A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | symgtgp 22707 | 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 22708 | A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 22710, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐽) | ||
Theorem | opnsubg 22709 | An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | clssubg 22710 | 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 22711 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺)) | ||
Theorem | cldsubg 22712 | 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 22713* | 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 22714* | The identity component, the connected component containing the identity element, is a closed (conncompcld 22035) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | tgpconncompss 22715* | 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 22716 | 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 22717 | 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 22718 | 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 22719 | Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre)) | ||
Theorem | tgpt0 22720 | Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2)) | ||
Theorem | qustgpopn 22721* | 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 22722* | Lemma for qustgp 22723. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐾 = (TopOpen‘𝐻) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) & ⊢ − = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgp 22723 | The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgphaus 22724 | 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 22725 | The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopMnd) | ||
Theorem | prdstgpd 22726 | The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopGrp) | ||
Syntax | ctsu 22727 | Extend class notation to include infinite group sums in a topological group. |
class tsums | ||
Definition | df-tsms 22728* | 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 15036) and Σg (df-gsum 16709), 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 22729* | 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 22730 | 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 22731* | 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 22732* | 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 22733 | 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 17929 etc. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) & ⊢ (𝜑 → (TopOpen‘𝐺) = (TopOpen‘𝐻)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐻 tsums 𝐹)) | ||
Theorem | eltsms 22734* | 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 22735* | 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 22736 | 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 22737* | 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 22738 | 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 22739 | One half of tgptsmscls 22751, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) | ||
Theorem | tsmsgsum 22740 | 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 22741 | 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 22742 | 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 22743* | 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 22744 | Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆)) | ||
Theorem | tsmsres 22745 | 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 22746 | 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 22747 | 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 22748 | 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 22749 | Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝐺 tsums (𝐼 ∘ 𝐹))) | ||
Theorem | tsmssub 22750 | The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻)) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻))) | ||
Theorem | tgptsmscls 22751 | A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 22711, 0nsg 18314. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) | ||
Theorem | tgptsmscld 22752 | 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 22753 | 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 22754* | Lemma for tsmsxp 22756. (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 22755* | Lemma for tsmsxp 22756. (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 22756* | Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19089 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 22754 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 22757 | The class of all topological division rings. |
class TopRing | ||
Syntax | ctdrg 22758 | The class of all topological division rings. |
class TopDRing | ||
Syntax | ctlm 22759 | The class of all topological modules. |
class TopMod | ||
Syntax | ctvc 22760 | The class of all topological vector spaces. |
class TopVec | ||
Definition | df-trg 22761 | 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 22762 | 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 22763 | 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 22764 | 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 22765 | Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ TopRing ↔ (𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd)) | ||
Theorem | trgtmd 22766 | The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ TopRing → 𝑀 ∈ TopMnd) | ||
Theorem | istdrg 22767 | Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s 𝑈) ∈ TopGrp)) | ||
Theorem | tdrgunit 22768 | 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 22769 | A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp) | ||
Theorem | trgtmd2 22770 | A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd) | ||
Theorem | trgtps 22771 | A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopSp) | ||
Theorem | trgring 22772 | A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Ring) | ||
Theorem | trggrp 22773 | A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Grp) | ||
Theorem | tdrgtrg 22774 | A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopRing) | ||
Theorem | tdrgdrng 22775 | A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ DivRing) | ||
Theorem | tdrgring 22776 | A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ Ring) | ||
Theorem | tdrgtmd 22777 | A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopMnd) | ||
Theorem | tdrgtps 22778 | A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopSp) | ||
Theorem | istdrg2 22779 | 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 22780 | 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 22781 | 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 22782 | 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 22783* | Continuity of ring multiplication; analogue of cnmpt12f 22267 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 22784* | Continuity of ring multiplication; analogue of cnmpt22f 22276 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 22785 | 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 22786 | 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 22787 | 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 22788 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) | ||
Theorem | tlmtps 22789 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | ||
Theorem | tlmlmod 22790 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) | ||
Theorem | tlmtrg 22791 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing) | ||
Theorem | tlmscatps 22792 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | ||
Theorem | istvc 22793 | 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 22794 | 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 22795* | Continuity of scalar multiplication; analogue of cnmpt12f 22267 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 22796* | Continuity of scalar multiplication; analogue of cnmpt22f 22276 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 22797 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) | ||
Theorem | tvctlm 22798 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod) | ||
Theorem | tvclmod 22799 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod) | ||
Theorem | tvclvec 22800 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |