Home | Metamath
Proof Explorer Theorem List (p. 225 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isngp2 22401 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸)) | ||
Theorem | isngp3 22402* | The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) | ||
Theorem | ngpgrp 22403 | A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) | ||
Theorem | ngpms 22404 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) | ||
Theorem | ngpxms 22405 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp) | ||
Theorem | ngptps 22406 | A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp) | ||
Theorem | ngpmet 22407 | The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | ngpds 22408 | Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))) | ||
Theorem | ngpdsr 22409 | Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐵 − 𝐴))) | ||
Theorem | ngpds2 22410 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐴 − 𝐵)𝐷 0 )) | ||
Theorem | ngpds2r 22411 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ((𝐵 − 𝐴)𝐷 0 )) | ||
Theorem | ngpds3 22412 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐴 − 𝐵))) | ||
Theorem | ngpds3r 22413 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = ( 0 𝐷(𝐵 − 𝐴))) | ||
Theorem | ngprcan 22414 | Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐶)𝐷(𝐵 + 𝐶)) = (𝐴𝐷𝐵)) | ||
Theorem | ngplcan 22415 | Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶 + 𝐴)𝐷(𝐶 + 𝐵)) = (𝐴𝐷𝐵)) | ||
Theorem | isngp4 22416* | Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦))) | ||
Theorem | ngpinvds 22417 | Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐼‘𝐴)𝐷(𝐼‘𝐵)) = (𝐴𝐷𝐵)) | ||
Theorem | ngpsubcan 22418 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵)) | ||
Theorem | nmf 22419 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ) | ||
Theorem | nmcl 22420 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) | ||
Theorem | nmge0 22421 | 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 22422 | 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 22423 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0) | ||
Theorem | nmrpcl 22424 | 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 22425 | 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 22426 | 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 22427 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴))) | ||
Theorem | nmrtri 22428 | 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 22429 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵))) | ||
Theorem | nmtri 22430 | 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 22431 | 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 22432* | 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 22433 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0) | ||
Theorem | nmgt0 22434 | 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 22435 | 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 22436 | 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 22437 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑀 = (norm‘𝐻) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴)) | ||
Theorem | subgnm2 22438 | 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 22439 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp) | ||
Theorem | ngptgp 22440 | 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 22441* | 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 22442 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ Rel dom toNrmGrp | ||
Theorem | tngval 22443 | 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 22444 | Lemma for tngbas 22445 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐸 = Slot 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐾 < 9 ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇)) | ||
Theorem | tngbas 22445 | The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐵 = (Base‘𝑇)) | ||
Theorem | tngplusg 22446 | The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → + = (+g‘𝑇)) | ||
Theorem | tng0 22447 | The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 0 = (0g‘𝑇)) | ||
Theorem | tngmulr 22448 | The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = (.r‘𝑇)) | ||
Theorem | tngsca 22449 | The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹 = (Scalar‘𝑇)) | ||
Theorem | tngvsca 22450 | The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘𝑇)) | ||
Theorem | tngip 22451 | The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → , = (·𝑖‘𝑇)) | ||
Theorem | tngds 22452 | The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∘ − ) = (dist‘𝑇)) | ||
Theorem | tngtset 22453 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇)) | ||
Theorem | tngtopn 22454 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇)) | ||
Theorem | tngnm 22455 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇)) | ||
Theorem | tngngp2 22456 | 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 22457* | 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 22458* | 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 22459 | 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 22460* | 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 22461 | 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 22462 | 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 22463 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
Theorem | isnrg 22464 | 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 22465 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴) | ||
Theorem | nrgngp 22466 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | ||
Theorem | nrgring 22467 | A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) | ||
Theorem | nmmul 22468 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | nrgdsdi 22469 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶))) | ||
Theorem | nrgdsdir 22470 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶))) | ||
Theorem | nm1 22471 | 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 22472 | 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 22473 | 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 22474 | 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 22475 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing)) | ||
Theorem | nrgtgp 22476 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp) | ||
Theorem | subrgnrg 22477 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing) | ||
Theorem | tngnrg 22478 | 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 22479* | 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 22480 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | nlmngp 22481 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | ||
Theorem | nlmlmod 22482 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) | ||
Theorem | nlmnrg 22483 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing) | ||
Theorem | nlmngp2 22484 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
Theorem | nlmdsdi 22485 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
Theorem | nlmdsdir 22486 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
Theorem | nlmmul0or 22487 | 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 22488 | 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 22489 | Lemma for nlmvscn 22491. Compare this proof with the similar elementary proof mulcn2 14326 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 22490* | Lemma for nlmvscn 22491. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
Theorem | nlmvscn 22491 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 22494 and nlmtlm 22498. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
Theorem | rlmnlm 22492 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
Theorem | rlmnm 22493 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
Theorem | nrgtrg 22494 | A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing) | ||
Theorem | nrginvrcnlem 22495* | Lemma for nrginvrcn 22496. Compare this proof with reccn2 14327, 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 22496 | 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 22497 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
Theorem | nlmtlm 22498 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
Theorem | isnvc 22499 | 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 22500 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |