| Metamath
Proof Explorer Theorem List (p. 248 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nlmngp2 24701 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
| Theorem | nlmdsdi 24702 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
| Theorem | nlmdsdir 24703 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
| Theorem | nlmmul0or 24704 | 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 24705 | 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 24706 | Lemma for nlmvscn 24708. Compare this proof with the similar elementary proof mulcn2 15632 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 24707* | Lemma for nlmvscn 24708. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
| Theorem | nlmvscn 24708 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24711 and nlmtlm 24715. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
| Theorem | rlmnlm 24709 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
| Theorem | rlmnm 24710 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
| ⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
| Theorem | nrgtrg 24711 | 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 24712* | Lemma for nrginvrcn 24713. Compare this proof with reccn2 15633, 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 24713 | 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 24714 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
| Theorem | nlmtlm 24715 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
| Theorem | isnvc 24716 | 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 24717 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) | ||
| Theorem | nvclvec 24718 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec) | ||
| Theorem | nvclmod 24719 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) | ||
| Theorem | isnvc2 24720 | 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 24721 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec) | ||
| Theorem | lssnlm 24722 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) | ||
| Theorem | lssnvc 24723 | 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 24724 | 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 24725 | 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 24726 | The operator norm function. |
| class normOp | ||
| Syntax | cnghm 24727 | The class of normed group homomorphisms. |
| class NGHom | ||
| Syntax | cnmhm 24728 | The class of normed module homomorphisms. |
| class NMHom | ||
| Definition | df-nmo 24729* | 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 24730* | 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 24731* | 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 24732 | 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 24733 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ Rel dom NGHom | ||
| Theorem | reldmnmhm 24734 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ Rel dom NMHom | ||
| Theorem | nmofval 24735* | Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁 = (𝑓 ∈ (𝑆 GrpHom 𝑇) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝑓‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < ))) | ||
| Theorem | nmoval 24736* | Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) = inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥))}, ℝ*, < )) | ||
| Theorem | nmogelb 24737* | Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ*) → (𝐴 ≤ (𝑁‘𝐹) ↔ ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → 𝐴 ≤ 𝑟))) | ||
| Theorem | nmolb 24738* | Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥)) → (𝑁‘𝐹) ≤ 𝐴)) | ||
| Theorem | nmolb2d 24739* | Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ NrmGrp) & ⊢ (𝜑 → 𝑇 ∈ NrmGrp) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (𝑀‘(𝐹‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) ⇒ ⊢ (𝜑 → (𝑁‘𝐹) ≤ 𝐴) | ||
| Theorem | nmof 24740 | The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁:(𝑆 GrpHom 𝑇)⟶ℝ*) | ||
| Theorem | nmocl 24741 | The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*) | ||
| Theorem | nmoge0 24742 | The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) | ||
| Theorem | nghmfval 24743 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ) | ||
| Theorem | isnghm 24744 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ))) | ||
| Theorem | isnghm2 24745 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ)) | ||
| Theorem | isnghm3 24746 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) < +∞)) | ||
| Theorem | bddnghm 24747 | A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
| Theorem | nghmcl 24748 | A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
| Theorem | nmoi 24749 | The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) | ||
| Theorem | nmoix 24750 | The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋))) | ||
| Theorem | nmoi2 24751 | The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 )) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹)) | ||
| Theorem | nmoleub 24752* | The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of 𝐹(𝑥) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ NrmGrp) & ⊢ (𝜑 → 𝑇 ∈ NrmGrp) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝑥 ≠ 0 → ((𝑀‘(𝐹‘𝑥)) / (𝐿‘𝑥)) ≤ 𝐴))) | ||
| Theorem | nghmrcl1 24753 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp) | ||
| Theorem | nghmrcl2 24754 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp) | ||
| Theorem | nghmghm 24755 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | nmo0 24756 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0) | ||
| Theorem | nmoeq0 24757 | The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) = 0 ↔ 𝐹 = (𝑉 × { 0 }))) | ||
| Theorem | nmoco 24758 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑈) & ⊢ 𝐿 = (𝑇 normOp 𝑈) & ⊢ 𝑀 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺))) | ||
| Theorem | nghmco 24759 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈)) | ||
| Theorem | nmotri 24760 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺))) | ||
| Theorem | nghmplusg 24761 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NGHom 𝑇)) | ||
| Theorem | 0nghm 24762 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇)) | ||
| Theorem | nmoid 24763 | The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑆) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉) → (𝑁‘( I ↾ 𝑉)) = 1) | ||
| Theorem | idnghm 24764 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) | ||
| Theorem | nmods 24765 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐶 = (dist‘𝑆) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐹‘𝐴)𝐷(𝐹‘𝐵)) ≤ ((𝑁‘𝐹) · (𝐴𝐶𝐵))) | ||
| Theorem | nghmcn 24766 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐾 = (TopOpen‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | isnmhm 24767 | A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | ||
| Theorem | nmhmrcl1 24768 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod) | ||
| Theorem | nmhmrcl2 24769 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod) | ||
| Theorem | nmhmlmhm 24770 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
| Theorem | nmhmnghm 24771 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
| Theorem | nmhmghm 24772 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | isnmhm2 24773 | A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ)) | ||
| Theorem | nmhmcl 24774 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
| Theorem | idnmhm 24775 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆)) | ||
| Theorem | 0nmhm 24776 | The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐹 = (Scalar‘𝑆) & ⊢ 𝐺 = (Scalar‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇)) | ||
| Theorem | nmhmco 24777 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈)) | ||
| Theorem | nmhmplusg 24778 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇)) | ||
| Theorem | qtopbaslem 24779 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ 𝑆 ⊆ ℝ* ⇒ ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases | ||
| Theorem | qtopbas 24780 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
| ⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases | ||
| Theorem | retopbas 24781 | A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.) |
| ⊢ ran (,) ∈ TopBases | ||
| Theorem | retop 24782 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
| ⊢ (topGen‘ran (,)) ∈ Top | ||
| Theorem | uniretop 24783 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
| ⊢ ℝ = ∪ (topGen‘ran (,)) | ||
| Theorem | retopon 24784 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ) | ||
| Theorem | retps 24785 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
| ⊢ 𝐾 = {〈(Base‘ndx), ℝ〉, 〈(TopSet‘ndx), (topGen‘ran (,))〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | iooretop 24786 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
| ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
| Theorem | icccld 24787 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | icopnfcld 24788 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | iocmnfcld 24789 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | qdensere 24790 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
| ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
| Theorem | cnmetdval 24791 | Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
| Theorem | cnmet 24792 | The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.) |
| ⊢ (abs ∘ − ) ∈ (Met‘ℂ) | ||
| Theorem | cnxmet 24793 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | ||
| Theorem | cnbl0 24794 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) | ||
| Theorem | cnblcld 24795* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) | ||
| Theorem | cnfldms 24796 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ MetSp | ||
| Theorem | cnfldxms 24797 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ ∞MetSp | ||
| Theorem | cnfldtps 24798 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ TopSp | ||
| Theorem | cnfldnm 24799 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ abs = (norm‘ℂfld) | ||
| Theorem | cnngp 24800 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ℂfld ∈ NrmGrp | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |