HomeTheorem List (p. 246 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 246 of 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ngpinvds 24501 | Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐼‘𝐴)𝐷(𝐼‘𝐵)) = (𝐴𝐷𝐵)) | ||
| Theorem | ngpsubcan 24502 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵)) | ||
| Theorem | nmf 24503 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ) | ||
| Theorem | nmcl 24504 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) | ||
| Theorem | nmge0 24505 | The norm of a normed group is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝑁‘𝐴)) | ||
| Theorem | nmeq0 24506 | The identity is the only element of the group with zero norm. First part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 24-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = 0 ↔ 𝐴 = 0 )) | ||
| Theorem | nmne0 24507 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0) | ||
| Theorem | nmrpcl 24508 | The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ∈ ℝ+) | ||
| Theorem | nminv 24509 | The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝐼‘𝐴)) = (𝑁‘𝐴)) | ||
| Theorem | nmmtri 24510 | The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) | ||
| Theorem | nmsub 24511 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴))) | ||
| Theorem | nmrtri 24512 | Reverse triangle inequality for the norm of a subtraction. Problem 3 of [Kreyszig] p. 64. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘((𝑁‘𝐴) − (𝑁‘𝐵))) ≤ (𝑁‘(𝐴 − 𝐵))) | ||
| Theorem | nm2dif 24513 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵))) | ||
| Theorem | nmtri 24514 | The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 + 𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) | ||
| Theorem | nmtri2 24515 | Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008.) (Revised by AV, 8-Oct-2021.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑁‘(𝐴 − 𝐶)) ≤ ((𝑁‘(𝐴 − 𝐵)) + (𝑁‘(𝐵 − 𝐶)))) | ||
| Theorem | ngpi 24516* | The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmGrp → (𝑊 ∈ Grp ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | ||
| Theorem | nm0 24517 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0) | ||
| Theorem | nmgt0 24518 | The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007.) (Revised by AV, 8-Oct-2021.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 0 ↔ 0 < (𝑁‘𝐴))) | ||
| Theorem | sgrim 24519 | The induced metric on a subgroup is the induced metric on the parent group equipped with a norm. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
| ⊢ 𝑋 = (𝑇 ↾s 𝑈) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐸 = (dist‘𝑋) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝐸 = 𝐷) | ||
| Theorem | sgrimval 24520 | The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
| ⊢ 𝑋 = (𝑇 ↾s 𝑈) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐸 = (dist‘𝑋) & ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑆 = (SubGrp‘𝑇) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝑈 ∈ 𝑆) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈)) → (𝐴𝐸𝐵) = (𝐴𝐷𝐵)) | ||
| Theorem | subgnm 24521 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑀 = (norm‘𝐻) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴)) | ||
| Theorem | subgnm2 24522 | A substructure assigns the same values to the norms of elements of a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑀 = (norm‘𝐻) ⇒ ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → (𝑀‘𝑋) = (𝑁‘𝑋)) | ||
| Theorem | subgngp 24523 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp) | ||
| Theorem | ngptgp 24524 | A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ TopGrp) | ||
| Theorem | ngppropd 24525* | Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ NrmGrp ↔ 𝐿 ∈ NrmGrp)) | ||
| Theorem | reldmtng 24526 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
| ⊢ Rel dom toNrmGrp | ||
| Theorem | tngval 24527 | Value of the function which augments a given structure 𝐺 with a norm 𝑁. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (𝑁 ∘ − ) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝑇 = ((𝐺 sSet ⟨(dist‘ndx), 𝐷⟩) sSet ⟨(TopSet‘ndx), 𝐽⟩)) | ||
| Theorem | tnglem 24528 | Lemma for tngbas 24529 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (TopSet‘ndx) & ⊢ (𝐸‘ndx) ≠ (dist‘ndx) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇)) | ||
| Theorem | tngbas 24529 | The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐵 = (Base‘𝑇)) | ||
| Theorem | tngplusg 24530 | The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → + = (+g‘𝑇)) | ||
| Theorem | tng0 24531 | The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 0 = (0g‘𝑇)) | ||
| Theorem | tngmulr 24532 | The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = (.r‘𝑇)) | ||
| Theorem | tngsca 24533 | The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹 = (Scalar‘𝑇)) | ||
| Theorem | tngvsca 24534 | The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘𝑇)) | ||
| Theorem | tngip 24535 | The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → , = (·𝑖‘𝑇)) | ||
| Theorem | tngds 24536 | The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof shortened by AV, 29-Oct-2024.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∘ − ) = (dist‘𝑇)) | ||
| Theorem | tngtset 24537 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇)) | ||
| Theorem | tngtopn 24538 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇)) | ||
| Theorem | tngnm 24539 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇)) | ||
| Theorem | tngngp2 24540 | A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋)))) | ||
| Theorem | tngngpd 24541* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑁:𝑋⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 )) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ⇒ ⊢ (𝜑 → 𝑇 ∈ NrmGrp) | ||
| Theorem | tngngp 24542* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) | ||
| Theorem | tnggrpr 24543 | If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp) | ||
| Theorem | tngngp3 24544* | Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) | ||
| Theorem | nrmtngdist 24545 | The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp (norm‘𝐺)) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋))) | ||
| Theorem | nrmtngnrm 24546 | The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp (norm‘𝐺)) ⇒ ⊢ (𝐺 ∈ NrmGrp → (𝑇 ∈ NrmGrp ∧ (norm‘𝑇) = (norm‘𝐺))) | ||
| Theorem | tngngpim 24547 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | isnrg 24548 | A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing ↔ (𝑅 ∈ NrmGrp ∧ 𝑁 ∈ 𝐴)) | ||
| Theorem | nrgabv 24549 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴) | ||
| Theorem | nrgngp 24550 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | ||
| Theorem | nrgring 24551 | A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) | ||
| Theorem | nmmul 24552 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | nrgdsdi 24553 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶))) | ||
| Theorem | nrgdsdir 24554 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶))) | ||
| Theorem | nm1 24555 | The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) → (𝑁‘ 1 ) = 1) | ||
| Theorem | unitnmn0 24556 | The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → (𝑁‘𝐴) ≠ 0) | ||
| Theorem | nminvr 24557 | The norm of an inverse in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → (𝑁‘(𝐼‘𝐴)) = (1 / (𝑁‘𝐴))) | ||
| Theorem | nmdvr 24558 | The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴 / 𝐵)) = ((𝑁‘𝐴) / (𝑁‘𝐵))) | ||
| Theorem | nrgdomn 24559 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing)) | ||
| Theorem | nrgtgp 24560 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp) | ||
| Theorem | subrgnrg 24561 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing) | ||
| Theorem | tngnrg 24562 | Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝑅 toNrmGrp 𝐹) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝑇 ∈ NrmRing) | ||
| Theorem | isnlm 24563* | A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 · 𝑦)) = ((𝐴‘𝑥) · (𝑁‘𝑦)))) | ||
| Theorem | nmvs 24564 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌))) | ||
| Theorem | nlmngp 24565 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | ||
| Theorem | nlmlmod 24566 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) | ||
| Theorem | nlmnrg 24567 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing) | ||
| Theorem | nlmngp2 24568 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
| Theorem | nlmdsdi 24569 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
| Theorem | nlmdsdir 24570 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
| Theorem | nlmmul0or 24571 | If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 𝑂 ∨ 𝐵 = 0 ))) | ||
| Theorem | sranlm 24572 | The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) ⇒ ⊢ ((𝑊 ∈ NrmRing ∧ 𝑆 ∈ (SubRing‘𝑊)) → 𝐴 ∈ NrmMod) | ||
| Theorem | nlmvscnlem2 24573 | Lemma for nlmvscn 24575. Compare this proof with the similar elementary proof mulcn2 15562 for continuity of multiplication on ℂ. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝐵𝐸𝐶) < 𝑈) & ⊢ (𝜑 → (𝑋𝐷𝑌) < 𝑇) ⇒ ⊢ (𝜑 → ((𝐵 · 𝑋)𝐷(𝐶 · 𝑌)) < 𝑅) | ||
| Theorem | nlmvscnlem1 24574* | Lemma for nlmvscn 24575. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
| Theorem | nlmvscn 24575 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24578 and nlmtlm 24582. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
| Theorem | rlmnlm 24576 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
| Theorem | rlmnm 24577 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
| ⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
| Theorem | nrgtrg 24578 | A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing) | ||
| Theorem | nrginvrcnlem 24579* | Lemma for nrginvrcn 24580. Compare this proof with reccn2 15563, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NrmRing) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝑇 = (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) | ||
| Theorem | nrginvrcn 24580 | The ring inverse function is continuous in a normed ring. (Note that this is true even in rings which are not division rings.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈))) | ||
| Theorem | nrgtdrg 24581 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
| Theorem | nlmtlm 24582 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
| Theorem | isnvc 24583 | A normed vector space is just a normed module which is algebraically a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmMod ∧ 𝑊 ∈ LVec)) | ||
| Theorem | nvcnlm 24584 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) | ||
| Theorem | nvclvec 24585 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec) | ||
| Theorem | nvclmod 24586 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) | ||
| Theorem | isnvc2 24587 | A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmMod ∧ 𝐹 ∈ DivRing)) | ||
| Theorem | nvctvc 24588 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec) | ||
| Theorem | lssnlm 24589 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) | ||
| Theorem | lssnvc 24590 | A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmVec) | ||
| Theorem | rlmnvc 24591 | The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → (ringLMod‘𝑅) ∈ NrmVec) | ||
| Theorem | ngpocelbl 24592 | Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007.) (Revised by AV, 14-Oct-2021.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ* ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃 + 𝐴) ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑁‘𝐴) < 𝑅)) | ||
| Syntax | cnmo 24593 | The operator norm function. |
| class normOp | ||
| Syntax | cnghm 24594 | The class of normed group homomorphisms. |
| class NGHom | ||
| Syntax | cnmhm 24595 | The class of normed module homomorphisms. |
| class NMHom | ||
| Definition | df-nmo 24596* | Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups ⟨𝑠, 𝑡⟩. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.) |
| ⊢ normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))) | ||
| Definition | df-nghm 24597* | Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ NGHom = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (◡(𝑠 normOp 𝑡) “ ℝ)) | ||
| Definition | df-nmhm 24598* | Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant 𝑐 such that... (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ NMHom = (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡))) | ||
| Theorem | nmoffn 24599 | The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
| ⊢ normOp Fn (NrmGrp × NrmGrp) | ||
| Theorem | reldmnghm 24600 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ Rel dom NGHom | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |