![]() |
Metamath
Proof Explorer Theorem List (p. 230 of 437) | < 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nlmvscnlem2 22901 | Lemma for nlmvscn 22903. Compare this proof with the similar elementary proof mulcn2 14738 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 22902* | Lemma for nlmvscn 22903. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
Theorem | nlmvscn 22903 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 22906 and nlmtlm 22910. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
Theorem | rlmnlm 22904 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
Theorem | rlmnm 22905 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
Theorem | nrgtrg 22906 | A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing) | ||
Theorem | nrginvrcnlem 22907* | Lemma for nrginvrcn 22908. Compare this proof with reccn2 14739, 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 22908 | 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 22909 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
Theorem | nlmtlm 22910 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
Theorem | isnvc 22911 | 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 22912 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) | ||
Theorem | nvclvec 22913 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec) | ||
Theorem | nvclmod 22914 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) | ||
Theorem | isnvc2 22915 | 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 22916 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec) | ||
Theorem | lssnlm 22917 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) | ||
Theorem | lssnvc 22918 | 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 22919 | 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 22920 | 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 22921 | The operator norm function. |
class normOp | ||
Syntax | cnghm 22922 | The class of normed group homomorphisms. |
class NGHom | ||
Syntax | cnmhm 22923 | The class of normed module homomorphisms. |
class NMHom | ||
Definition | df-nmo 22924* | 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 22925* | 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 22926* | 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 22927 | 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 22928 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ Rel dom NGHom | ||
Theorem | reldmnmhm 22929 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ Rel dom NMHom | ||
Theorem | nmofval 22930* | 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 22931* | 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 22932* | 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 22933* | 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 22934* | 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 22935 | 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 22936 | The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*) | ||
Theorem | nmoge0 22937 | The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) | ||
Theorem | nghmfval 22938 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ) | ||
Theorem | isnghm 22939 | 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 22940 | 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 22941 | 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 22942 | A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nghmcl 22943 | A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
Theorem | nmoi 22944 | 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 22945 | 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 22946 | 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 22947* | 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 22948 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp) | ||
Theorem | nghmrcl2 22949 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp) | ||
Theorem | nghmghm 22950 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | nmo0 22951 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0) | ||
Theorem | nmoeq0 22952 | 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 22953 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑈) & ⊢ 𝐿 = (𝑇 normOp 𝑈) & ⊢ 𝑀 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺))) | ||
Theorem | nghmco 22954 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈)) | ||
Theorem | nmotri 22955 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘𝑓 + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺))) | ||
Theorem | nghmplusg 22956 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | 0nghm 22957 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmoid 22958 | 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 22959 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) | ||
Theorem | nmods 22960 | 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 22961 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐾 = (TopOpen‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | isnmhm 22962 | 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 22963 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod) | ||
Theorem | nmhmrcl2 22964 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod) | ||
Theorem | nmhmlmhm 22965 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | nmhmnghm 22966 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmhmghm 22967 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | isnmhm2 22968 | 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 22969 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
Theorem | idnmhm 22970 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆)) | ||
Theorem | 0nmhm 22971 | 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 22972 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈)) | ||
Theorem | nmhmplusg 22973 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑆 NMHom 𝑇)) | ||
Theorem | qtopbaslem 22974 | 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 22975 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases | ||
Theorem | retopbas 22976 | 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 22977 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ (topGen‘ran (,)) ∈ Top | ||
Theorem | uniretop 22978 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ ℝ = ∪ (topGen‘ran (,)) | ||
Theorem | retopon 22979 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ) | ||
Theorem | retps 22980 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉, 〈(TopSet‘ndx), (topGen‘ran (,))〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | iooretop 22981 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
Theorem | icccld 22982 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | icopnfcld 22983 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | iocmnfcld 22984 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | qdensere 22985 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
Theorem | cnmetdval 22986 | 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 22987 | 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 22988 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | ||
Theorem | cnbl0 22989 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) | ||
Theorem | cnblcld 22990* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) | ||
Theorem | cnfldms 22991 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ MetSp | ||
Theorem | cnfldxms 22992 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ ∞MetSp | ||
Theorem | cnfldtps 22993 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ TopSp | ||
Theorem | cnfldnm 22994 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ abs = (norm‘ℂfld) | ||
Theorem | cnngp 22995 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ ℂfld ∈ NrmGrp | ||
Theorem | cnnrg 22996 | The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ ℂfld ∈ NrmRing | ||
Theorem | cnfldtopn 22997 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 = (MetOpen‘(abs ∘ − )) | ||
Theorem | cnfldtopon 22998 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ (TopOn‘ℂ) | ||
Theorem | cnfldtop 22999 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Top | ||
Theorem | cnfldhaus 23000 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Haus |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |