HomeTheorem List (p. 247 of 504)
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. 247 of 504) | < 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-31011) |
Hilbert Space Explorer
(31012-32534) |
Users' Mathboxes
(32535-50309) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ngpsubcan 24601 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵)) | ||
| Theorem | nmf 24602 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ) | ||
| Theorem | nmcl 24603 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) | ||
| Theorem | nmge0 24604 | 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 24605 | 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 24606 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0) | ||
| Theorem | nmrpcl 24607 | 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 24608 | 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 24609 | 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 24610 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴))) | ||
| Theorem | nmrtri 24611 | 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 24612 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵))) | ||
| Theorem | nmtri 24613 | 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 24614 | 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 24615* | 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 24616 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0) | ||
| Theorem | nmgt0 24617 | 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 24618 | 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 24619 | 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 24620 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑀 = (norm‘𝐻) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴)) | ||
| Theorem | subgnm2 24621 | 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 24622 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp) | ||
| Theorem | ngptgp 24623 | 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 24624* | 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 24625 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
| ⊢ Rel dom toNrmGrp | ||
| Theorem | tngval 24626 | 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 24627 | Lemma for tngbas 24628 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 24628 | 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 24629 | 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 24630 | 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 24631 | 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 24632 | 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 24633 | 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 24634 | 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 24635 | 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 24636 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇)) | ||
| Theorem | tngtopn 24637 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇)) | ||
| Theorem | tngnm 24638 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇)) | ||
| Theorem | tngngp2 24639 | 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 24640* | 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 24641* | 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 24642 | 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 24643* | 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 24644 | 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 24645 | 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 24646 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | isnrg 24647 | 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 24648 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴) | ||
| Theorem | nrgngp 24649 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | ||
| Theorem | nrgring 24650 | A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) | ||
| Theorem | nmmul 24651 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | nrgdsdi 24652 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶))) | ||
| Theorem | nrgdsdir 24653 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶))) | ||
| Theorem | nm1 24654 | 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 24655 | 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 24656 | 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 24657 | 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 24658 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing)) | ||
| Theorem | nrgtgp 24659 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp) | ||
| Theorem | subrgnrg 24660 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing) | ||
| Theorem | tngnrg 24661 | 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 24662* | 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 24663 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌))) | ||
| Theorem | nlmngp 24664 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | ||
| Theorem | nlmlmod 24665 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) | ||
| Theorem | nlmnrg 24666 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing) | ||
| Theorem | nlmngp2 24667 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
| Theorem | nlmdsdi 24668 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
| Theorem | nlmdsdir 24669 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
| Theorem | nlmmul0or 24670 | 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 24671 | 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 24672 | Lemma for nlmvscn 24674. Compare this proof with the similar elementary proof mulcn2 15553 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 24673* | Lemma for nlmvscn 24674. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
| Theorem | nlmvscn 24674 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24677 and nlmtlm 24681. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
| Theorem | rlmnlm 24675 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
| Theorem | rlmnm 24676 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
| ⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
| Theorem | nrgtrg 24677 | 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 24678* | Lemma for nrginvrcn 24679. Compare this proof with reccn2 15554, 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 24679 | 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 24680 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
| Theorem | nlmtlm 24681 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
| Theorem | isnvc 24682 | 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 24683 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) | ||
| Theorem | nvclvec 24684 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec) | ||
| Theorem | nvclmod 24685 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) | ||
| Theorem | isnvc2 24686 | 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 24687 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec) | ||
| Theorem | lssnlm 24688 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) | ||
| Theorem | lssnvc 24689 | 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 24690 | 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 24691 | 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 24692 | The operator norm function. |
| class normOp | ||
| Syntax | cnghm 24693 | The class of normed group homomorphisms. |
| class NGHom | ||
| Syntax | cnmhm 24694 | The class of normed module homomorphisms. |
| class NMHom | ||
| Definition | df-nmo 24695* | 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 24696* | 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 24697* | 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 24698 | 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 24699 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ Rel dom NGHom | ||
| Theorem | reldmnmhm 24700 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ Rel dom NMHom | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |