Home | Metamath
Proof Explorer Theorem List (p. 223 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-nlm 22201* | 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.) |
⊢ NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))} | ||
Definition | df-nvc 22202 | A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ NrmVec = (NrmMod ∩ LVec) | ||
Theorem | nmfval 22203* | The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) | ||
Theorem | nmval 22204 | The value of the norm function. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝑁‘𝐴) = (𝐴𝐷 0 )) | ||
Theorem | nmfval2 22205* | The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 ))) | ||
Theorem | nmval2 22206 | The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐸 0 )) | ||
Theorem | nmf2 22207 | The norm is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) | ||
Theorem | nmpropd 22208 | Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (dist‘𝐾) = (dist‘𝐿)) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
Theorem | nmpropd2 22209* | Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐾 ∈ Grp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
Theorem | isngp 22210 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷)) | ||
Theorem | isngp2 22211 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸)) | ||
Theorem | isngp3 22212* | The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) | ||
Theorem | ngpgrp 22213 | A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) | ||
Theorem | ngpms 22214 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) | ||
Theorem | ngpxms 22215 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp) | ||
Theorem | ngptps 22216 | A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp) | ||
Theorem | ngpmet 22217 | 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 22218 | 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 22219 | 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 22220 | 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 22221 | 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 22222 | 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 22223 | 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 22224 | Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐶)𝐷(𝐵 + 𝐶)) = (𝐴𝐷𝐵)) | ||
Theorem | ngplcan 22225 | Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶 + 𝐴)𝐷(𝐶 + 𝐵)) = (𝐴𝐷𝐵)) | ||
Theorem | isngp4 22226* | 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 22227 | Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐼‘𝐴)𝐷(𝐼‘𝐵)) = (𝐴𝐷𝐵)) | ||
Theorem | ngpsubcan 22228 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴 − 𝐶)𝐷(𝐵 − 𝐶)) = (𝐴𝐷𝐵)) | ||
Theorem | nmf 22229 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁:𝑋⟶ℝ) | ||
Theorem | nmcl 22230 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) | ||
Theorem | nmge0 22231 | 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 22232 | 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 22233 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → (𝑁‘𝐴) ≠ 0) | ||
Theorem | nmrpcl 22234 | 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 22235 | 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 22236 | 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 22237 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 − 𝐵)) = (𝑁‘(𝐵 − 𝐴))) | ||
Theorem | nmrtri 22238 | 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 22239 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝐵)) ≤ (𝑁‘(𝐴 − 𝐵))) | ||
Theorem | nmtri 22240 | 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 22241 | 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 22242* | 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 22243 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp → (𝑁‘ 0 ) = 0) | ||
Theorem | nmgt0 22244 | 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 22245 | 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 22246 | 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 22247 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑀 = (norm‘𝐻) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝑀 = (𝑁 ↾ 𝐴)) | ||
Theorem | subgnm2 22248 | 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 22249 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp) | ||
Theorem | ngptgp 22250 | 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 22251* | 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 22252 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ Rel dom toNrmGrp | ||
Theorem | tngval 22253 | 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 22254 | Lemma for tngbas 22255 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐸 = Slot 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐾 < 9 ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐸‘𝐺) = (𝐸‘𝑇)) | ||
Theorem | tngbas 22255 | The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐵 = (Base‘𝑇)) | ||
Theorem | tngplusg 22256 | The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → + = (+g‘𝑇)) | ||
Theorem | tng0 22257 | The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 0 = (0g‘𝑇)) | ||
Theorem | tngmulr 22258 | The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = (.r‘𝑇)) | ||
Theorem | tngsca 22259 | The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹 = (Scalar‘𝑇)) | ||
Theorem | tngvsca 22260 | The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘𝑇)) | ||
Theorem | tngip 22261 | The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → , = (·𝑖‘𝑇)) | ||
Theorem | tngds 22262 | The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∘ − ) = (dist‘𝑇)) | ||
Theorem | tngtset 22263 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopSet‘𝑇)) | ||
Theorem | tngtopn 22264 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝐷 = (dist‘𝑇) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → 𝐽 = (TopOpen‘𝑇)) | ||
Theorem | tngnm 22265 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶𝐴) → 𝑁 = (norm‘𝑇)) | ||
Theorem | tngngp2 22266 | 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 22267* | 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 22268* | 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 22269 | 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 22270* | 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 22271 | 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 22272 | 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 22273 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
Theorem | isnrg 22274 | 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 22275 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝑅 ∈ NrmRing → 𝑁 ∈ 𝐴) | ||
Theorem | nrgngp 22276 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | ||
Theorem | nrgring 22277 | A normed ring is a ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) | ||
Theorem | nmmul 22278 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴 · 𝐵)) = ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | nrgdsdi 22279 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝑁‘𝐴) · (𝐵𝐷𝐶)) = ((𝐴 · 𝐵)𝐷(𝐴 · 𝐶))) | ||
Theorem | nrgdsdir 22280 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑁 = (norm‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐷 = (dist‘𝑅) ⇒ ⊢ ((𝑅 ∈ NrmRing ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵) · (𝑁‘𝐶)) = ((𝐴 · 𝐶)𝐷(𝐵 · 𝐶))) | ||
Theorem | nm1 22281 | 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 22282 | 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 22283 | 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 22284 | 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 22285 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing)) | ||
Theorem | nrgtgp 22286 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp) | ||
Theorem | subrgnrg 22287 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing) | ||
Theorem | tngnrg 22288 | 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 22289* | 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 22290 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | nlmngp 22291 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | ||
Theorem | nlmlmod 22292 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) | ||
Theorem | nlmnrg 22293 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing) | ||
Theorem | nlmngp2 22294 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
Theorem | nlmdsdi 22295 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
Theorem | nlmdsdir 22296 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
Theorem | nlmmul0or 22297 | 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 22298 | 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 22299 | Lemma for nlmvscn 22301. Compare this proof with the similar elementary proof mulcn2 14174 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 22300* | Lemma for nlmvscn 22301. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |