![]() |
Metamath
Proof Explorer Theorem List (p. 242 of 486) | < 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: | ![]() (1-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clssubg 24101 | 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 24102 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺)) | ||
Theorem | cldsubg 24103 | 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 24104* | 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 24105* | The identity component, the connected component containing the identity element, is a closed (conncompcld 23426) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | tgpconncompss 24106* | 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 24107 | 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 24108 | 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 24109 | 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 24110 | Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre)) | ||
Theorem | tgpt0 24111 | Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2)) | ||
Theorem | qustgpopn 24112* | 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 24113* | Lemma for qustgp 24114. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐾 = (TopOpen‘𝐻) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) & ⊢ − = (𝑧 ∈ 𝑋, 𝑤 ∈ 𝑋 ↦ [(𝑧(-g‘𝐺)𝑤)](𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgp 24114 | The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑌 ∈ (NrmSGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | qustgphaus 24115 | 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 24116 | The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopMnd) | ||
Theorem | prdstgpd 24117 | The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopGrp) | ||
Syntax | ctsu 24118 | Extend class notation to include infinite group sums in a topological group. |
class tsums | ||
Definition | df-tsms 24119* | 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 15686) and Σg (df-gsum 17452), 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 24120* | 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 24121 | 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 24122* | 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 24123* | 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 24124 | 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 18747 etc. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) & ⊢ (𝜑 → (TopOpen‘𝐺) = (TopOpen‘𝐻)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐻 tsums 𝐹)) | ||
Theorem | eltsms 24125* | 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 24126* | 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 24127 | 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 24128* | 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 24129 | 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 24130 | One half of tgptsmscls 24142, true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘{𝑋}) ⊆ (𝐺 tsums 𝐹)) | ||
Theorem | tsmsgsum 24131 | 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 24132 | 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 24133 | 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 24134* | 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 24135 | Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopSp) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆)) | ||
Theorem | tsmsres 24136 | 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 24137 | 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 24138 | 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 24139 | 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 24140 | Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝐺 tsums (𝐼 ∘ 𝐹))) | ||
Theorem | tsmssub 24141 | The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻)) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻))) | ||
Theorem | tgptsmscls 24142 | A sum in a topological group is uniquely determined up to a coset of cls({0}), which is a normal subgroup by clsnsg 24102, 0nsg 19159. (Contributed by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{𝑋})) | ||
Theorem | tgptsmscld 24143 | 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 24144 | 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 24145* | Lemma for tsmsxp 24147. (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 24146* | Lemma for tsmsxp 24147. (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 24147* | Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19970 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24145 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 24148 | The class of all topological division rings. |
class TopRing | ||
Syntax | ctdrg 24149 | The class of all topological division rings. |
class TopDRing | ||
Syntax | ctlm 24150 | The class of all topological modules. |
class TopMod | ||
Syntax | ctvc 24151 | The class of all topological vector spaces. |
class TopVec | ||
Definition | df-trg 24152 | 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 24153 | 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 24154 | 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 24155 | 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 24156 | Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ TopRing ↔ (𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd)) | ||
Theorem | trgtmd 24157 | The multiplicative monoid of a topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ TopRing → 𝑀 ∈ TopMnd) | ||
Theorem | istdrg 24158 | Express the predicate "𝑅 is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s 𝑈) ∈ TopGrp)) | ||
Theorem | tdrgunit 24159 | 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 24160 | A topological ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopGrp) | ||
Theorem | trgtmd2 24161 | A topological ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd) | ||
Theorem | trgtps 24162 | A topological ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopSp) | ||
Theorem | trgring 24163 | A topological ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Ring) | ||
Theorem | trggrp 24164 | A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ Grp) | ||
Theorem | tdrgtrg 24165 | A topological division ring is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopRing) | ||
Theorem | tdrgdrng 24166 | A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ DivRing) | ||
Theorem | tdrgring 24167 | A topological division ring is a ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ Ring) | ||
Theorem | tdrgtmd 24168 | A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopMnd) | ||
Theorem | tdrgtps 24169 | A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopSp) | ||
Theorem | istdrg2 24170 | 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 24171 | 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 24172 | 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 24173 | 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 24174* | Continuity of ring multiplication; analogue of cnmpt12f 23658 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 24175* | Continuity of ring multiplication; analogue of cnmpt22f 23667 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 24176 | 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 24177 | 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 24178 | 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 24179 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) | ||
Theorem | tlmtps 24180 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | ||
Theorem | tlmlmod 24181 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) | ||
Theorem | tlmtrg 24182 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing) | ||
Theorem | tlmscatps 24183 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | ||
Theorem | istvc 24184 | 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 24185 | 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 24186* | Continuity of scalar multiplication; analogue of cnmpt12f 23658 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 24187* | Continuity of scalar multiplication; analogue of cnmpt22f 23667 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 24188 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) | ||
Theorem | tvctlm 24189 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod) | ||
Theorem | tvclmod 24190 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod) | ||
Theorem | tvclvec 24191 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec) | ||
Syntax | cust 24192 | Extend class notation with the class function of uniform structures. |
class UnifOn | ||
Definition | df-ust 24193* | Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.) |
⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))}) | ||
Theorem | ustfn 24194 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ UnifOn Fn V | ||
Theorem | ustval 24195* | The class of all uniform structures for a base 𝑋. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))}) | ||
Theorem | isust 24196* | The predicate "𝑈 is a uniform structure with base 𝑋". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))))) | ||
Theorem | ustssxp 24197 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋)) | ||
Theorem | ustssel 24198 | A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ (𝑋 × 𝑋)) → (𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈)) | ||
Theorem | ustbasel 24199 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈) | ||
Theorem | ustincl 24200 | A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑉 ∩ 𝑊) ∈ 𝑈) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |