![]() |
Metamath
Proof Explorer Theorem List (p. 247 of 483) | < 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-30741) |
![]() (30742-32264) |
![]() (32265-48238) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nrgdomn 24601 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing)) | ||
Theorem | nrgtgp 24602 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp) | ||
Theorem | subrgnrg 24603 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ ((𝐺 ∈ NrmRing ∧ 𝐴 ∈ (SubRing‘𝐺)) → 𝐻 ∈ NrmRing) | ||
Theorem | tngnrg 24604 | 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 24605* | 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 24606 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑁‘(𝑋 · 𝑌)) = ((𝐴‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | nlmngp 24607 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) | ||
Theorem | nlmlmod 24608 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod) | ||
Theorem | nlmnrg 24609 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing) | ||
Theorem | nlmngp2 24610 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp) | ||
Theorem | nlmdsdi 24611 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝐴‘𝑋) · (𝑌𝐷𝑍)) = ((𝑋 · 𝑌)𝐷(𝑋 · 𝑍))) | ||
Theorem | nlmdsdir 24612 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉)) → ((𝑋𝐸𝑌) · (𝑁‘𝑍)) = ((𝑋 · 𝑍)𝐷(𝑌 · 𝑍))) | ||
Theorem | nlmmul0or 24613 | 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 24614 | 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 24615 | Lemma for nlmvscn 24617. Compare this proof with the similar elementary proof mulcn2 15573 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 24616* | Lemma for nlmvscn 24617. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (dist‘𝐹) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐴 = (norm‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝐴‘𝐵) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝑋) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ NrmMod) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑉 (((𝐵𝐸𝑥) < 𝑟 ∧ (𝑋𝐷𝑦) < 𝑟) → ((𝐵 · 𝑋)𝐷(𝑥 · 𝑦)) < 𝑅)) | ||
Theorem | nlmvscn 24617 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24620 and nlmtlm 24624. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·sf ‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘𝐹) ⇒ ⊢ (𝑊 ∈ NrmMod → · ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
Theorem | rlmnlm 24618 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod) | ||
Theorem | rlmnm 24619 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
⊢ (norm‘𝑅) = (norm‘(ringLMod‘𝑅)) | ||
Theorem | nrgtrg 24620 | 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 24621* | Lemma for nrginvrcn 24622. Compare this proof with reccn2 15574, 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 24622 | 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 24623 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) | ||
Theorem | nlmtlm 24624 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ TopMod) | ||
Theorem | isnvc 24625 | 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 24626 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod) | ||
Theorem | nvclvec 24627 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LVec) | ||
Theorem | nvclmod 24628 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ LMod) | ||
Theorem | isnvc2 24629 | 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 24630 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝑊 ∈ NrmVec → 𝑊 ∈ TopVec) | ||
Theorem | lssnlm 24631 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) | ||
Theorem | lssnvc 24632 | 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 24633 | 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 24634 | 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 24635 | The operator norm function. |
class normOp | ||
Syntax | cnghm 24636 | The class of normed group homomorphisms. |
class NGHom | ||
Syntax | cnmhm 24637 | The class of normed module homomorphisms. |
class NMHom | ||
Definition | df-nmo 24638* | 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 24639* | 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 24640* | 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 24641 | 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 24642 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ Rel dom NGHom | ||
Theorem | reldmnmhm 24643 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ Rel dom NMHom | ||
Theorem | nmofval 24644* | 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 24645* | 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 24646* | 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 24647* | 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 24648* | 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 24649 | 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 24650 | The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈ ℝ*) | ||
Theorem | nmoge0 24651 | The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) | ||
Theorem | nghmfval 24652 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝑆 NGHom 𝑇) = (◡𝑁 “ ℝ) | ||
Theorem | isnghm 24653 | 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 24654 | 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 24655 | 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 24656 | A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝐴 ∈ ℝ ∧ (𝑁‘𝐹) ≤ 𝐴)) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nghmcl 24657 | A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
Theorem | nmoi 24658 | 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 24659 | 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 24660 | 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 24661* | 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 24662 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp) | ||
Theorem | nghmrcl2 24663 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp) | ||
Theorem | nghmghm 24664 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | nmo0 24665 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0) | ||
Theorem | nmoeq0 24666 | 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 24667 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑈) & ⊢ 𝐿 = (𝑇 normOp 𝑈) & ⊢ 𝑀 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺))) | ||
Theorem | nghmco 24668 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈)) | ||
Theorem | nmotri 24669 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺))) | ||
Theorem | nghmplusg 24670 | 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 24671 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmoid 24672 | 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 24673 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) | ||
Theorem | nmods 24674 | 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 24675 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐾 = (TopOpen‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | isnmhm 24676 | 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 24677 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod) | ||
Theorem | nmhmrcl2 24678 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod) | ||
Theorem | nmhmlmhm 24679 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | nmhmnghm 24680 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmhmghm 24681 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | isnmhm2 24682 | 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 24683 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
Theorem | idnmhm 24684 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆)) | ||
Theorem | 0nmhm 24685 | 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 24686 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈)) | ||
Theorem | nmhmplusg 24687 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇)) | ||
Theorem | qtopbaslem 24688 | 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 24689 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases | ||
Theorem | retopbas 24690 | 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 24691 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ (topGen‘ran (,)) ∈ Top | ||
Theorem | uniretop 24692 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ ℝ = ∪ (topGen‘ran (,)) | ||
Theorem | retopon 24693 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ) | ||
Theorem | retps 24694 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉, 〈(TopSet‘ndx), (topGen‘ran (,))〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | iooretop 24695 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
Theorem | icccld 24696 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | icopnfcld 24697 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | iocmnfcld 24698 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | qdensere 24699 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
Theorem | cnmetdval 24700 | 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‘(𝐴 − 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |