| Metamath
Proof Explorer Theorem List (p. 308 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 | cnnvm 30701 | The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 + , · 〉, abs〉 ⇒ ⊢ − = ( −𝑣 ‘𝑈) | ||
| Theorem | elimnv 30702 | Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋 | ||
| Theorem | elimnvu 30703 | Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.) |
| ⊢ if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉, abs〉) ∈ NrmCVec | ||
| Theorem | imsval 30704 | Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐷 = (𝑁 ∘ 𝑀)) | ||
| Theorem | imsdval 30705 | Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝑀𝐵))) | ||
| Theorem | imsdval2 30706 | Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝐺(-1𝑆𝐵)))) | ||
| Theorem | nvnd 30707 | The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐷𝑍)) | ||
| Theorem | imsdf 30708 | Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | imsmetlem 30709 | Lemma for imsmet 30710. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = (inv‘𝐺) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
| Theorem | imsmet 30710 | The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | imsxmet 30711 | The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | cnims 30712 | The metric induced on the complex numbers. cnmet 24792 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by NM, 15-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 = 〈〈 + , · 〉, abs〉 & ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ 𝐷 = (IndMet‘𝑈) | ||
| Theorem | vacn 30713 | Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
| Theorem | nmcvcn 30714 | The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | nmcnc 30715 | The norm of a normed complex vector space is a continuous function to ℂ. (For ℝ, see nmcvcn 30714.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | smcnlem 30716* | Lemma for smcn 30717. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ⇒ ⊢ 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
| Theorem | smcn 30717 | Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | ||
| Theorem | vmcn 30718 | Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑀 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
| Syntax | cdip 30719 | Extend class notation with the class inner product functions. |
| class ·𝑖OLD | ||
| Definition | df-dip 30720* | Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is (1st ‘𝑤), the scalar product is (2nd ‘𝑤), and the norm is 𝑛. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.) |
| ⊢ ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4))) | ||
| Theorem | dipfval 30721* | The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑃 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4))) | ||
| Theorem | ipval 30722* | Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, the norm is 𝑁, and the set of vectors is 𝑋. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) / 4)) | ||
| Theorem | ipval2lem2 30723 | Lemma for ipval3 30728. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℝ) | ||
| Theorem | ipval2lem3 30724 | Lemma for ipval3 30728. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ) | ||
| Theorem | ipval2lem4 30725 | Lemma for ipval3 30728. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ) | ||
| Theorem | ipval2 30726 | Expansion of the inner product value ipval 30722. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2)))) / 4)) | ||
| Theorem | 4ipval2 30727 | Four times the inner product value ipval3 30728, useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴𝑃𝐵)) = ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2))))) | ||
| Theorem | ipval3 30728 | Expansion of the inner product value ipval 30722. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝑀𝐵))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝑀(i𝑆𝐵)))↑2)))) / 4)) | ||
| Theorem | ipidsq 30729 | The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = ((𝑁‘𝐴)↑2)) | ||
| Theorem | ipnm 30730 | Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴))) | ||
| Theorem | dipcl 30731 | An inner product is a complex number. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ) | ||
| Theorem | ipf 30732 | Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑃:(𝑋 × 𝑋)⟶ℂ) | ||
| Theorem | dipcj 30733 | The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∗‘(𝐴𝑃𝐵)) = (𝐵𝑃𝐴)) | ||
| Theorem | ipipcj 30734 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2)) | ||
| Theorem | diporthcom 30735 | Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) = 0 ↔ (𝐵𝑃𝐴) = 0)) | ||
| Theorem | dip0r 30736 | Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0) | ||
| Theorem | dip0l 30737 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑍𝑃𝐴) = 0) | ||
| Theorem | ipz 30738 | The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝐴𝑃𝐴) = 0 ↔ 𝐴 = 𝑍)) | ||
| Theorem | dipcn 30739 | Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑃 ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Syntax | css 30740 | Extend class notation with the class of all subspaces of normed complex vector spaces. |
| class SubSp | ||
| Definition | df-ssp 30741* | Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))}) | ||
| Theorem | sspval 30742* | The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)}) | ||
| Theorem | isssp 30743 | The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐹 = ( +𝑣 ‘𝑊) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁)))) | ||
| Theorem | sspid 30744 | A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻) | ||
| Theorem | sspnv 30745 | A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) | ||
| Theorem | sspba 30746 | The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ 𝑋) | ||
| Theorem | sspg 30747 | Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐹 = ( +𝑣 ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) | ||
| Theorem | sspgval 30748 | Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐹 = ( +𝑣 ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) | ||
| Theorem | ssps 30749 | Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑆 ↾ (ℂ × 𝑌))) | ||
| Theorem | sspsval 30750 | Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑌)) → (𝐴𝑅𝐵) = (𝐴𝑆𝐵)) | ||
| Theorem | sspmlem 30751* | Lemma for sspm 30753 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) & ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) & ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅) & ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) | ||
| Theorem | sspmval 30752 | Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝐿 = ( −𝑣 ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐿𝐵) = (𝐴𝑀𝐵)) | ||
| Theorem | sspm 30753 | Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝐿 = ( −𝑣 ‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐿 = (𝑀 ↾ (𝑌 × 𝑌))) | ||
| Theorem | sspz 30754 | The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑄 = (0vec‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑄 = 𝑍) | ||
| Theorem | sspn 30755 | The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑁 ↾ 𝑌)) | ||
| Theorem | sspnval 30756 | The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝐴 ∈ 𝑌) → (𝑀‘𝐴) = (𝑁‘𝐴)) | ||
| Theorem | sspimsval 30757 | The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐶𝐵) = (𝐴𝐷𝐵)) | ||
| Theorem | sspims 30758 | The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐶 = (𝐷 ↾ (𝑌 × 𝑌))) | ||
| Syntax | clno 30759 | Extend class notation with the class of linear operators on normed complex vector spaces. |
| class LnOp | ||
| Syntax | cnmoo 30760 | Extend class notation with the class of operator norms on normed complex vector spaces. |
| class normOpOLD | ||
| Syntax | cblo 30761 | Extend class notation with the class of bounded linear operators on normed complex vector spaces. |
| class BLnOp | ||
| Syntax | c0o 30762 | Extend class notation with the class of zero operators on normed complex vector spaces. |
| class 0op | ||
| Definition | df-lno 30763* | Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e., the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))}) | ||
| Definition | df-nmoo 30764* | Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces 〈𝑢, 𝑤〉. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))) | ||
| Definition | df-blo 30765* | Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}) | ||
| Definition | df-0o 30766* | Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)})) | ||
| Syntax | caj 30767 | Adjoint of an operator. |
| class adj | ||
| Syntax | chmo 30768 | Set of Hermitional (self-adjoint) operators. |
| class HmOp | ||
| Definition | df-aj 30769* | Define the adjoint of an operator (if it exists). The domain of 𝑈adj𝑊 is the set of all operators from 𝑈 to 𝑊 that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that 𝑈 and 𝑊 be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) | ||
| Definition | df-hmo 30770* | Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}) | ||
| Theorem | lnoval 30771* | The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐿 = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))}) | ||
| Theorem | islno 30772* | The predicate "is a linear operator." (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑇‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑇‘𝑦))𝐻(𝑇‘𝑧))))) | ||
| Theorem | lnolin 30773 | Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) | ||
| Theorem | lnof 30774 | A linear operator is a mapping. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌) | ||
| Theorem | lno0 30775 | The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑄 = (0vec‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑄) = 𝑍) | ||
| Theorem | lnocoi 30776 | The composition of two linear operators is linear. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑀 = (𝑊 LnOp 𝑋) & ⊢ 𝑁 = (𝑈 LnOp 𝑋) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑋 ∈ NrmCVec & ⊢ 𝑆 ∈ 𝐿 & ⊢ 𝑇 ∈ 𝑀 ⇒ ⊢ (𝑇 ∘ 𝑆) ∈ 𝑁 | ||
| Theorem | lnoadd 30777 | Addition property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝐺𝐵)) = ((𝑇‘𝐴)𝐻(𝑇‘𝐵))) | ||
| Theorem | lnosub 30778 | Subtraction property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = ( −𝑣 ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑀𝐵)) = ((𝑇‘𝐴)𝑁(𝑇‘𝐵))) | ||
| Theorem | lnomul 30779 | Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑅𝐵)) = (𝐴𝑆(𝑇‘𝐵))) | ||
| Theorem | nvo00 30780 | Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍})) | ||
| Theorem | nmoofval 30781* | The operator norm function. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑁 = (𝑡 ∈ (𝑌 ↑m 𝑋) ↦ sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑡‘𝑧)))}, ℝ*, < ))) | ||
| Theorem | nmooval 30782* | The operator norm function. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < )) | ||
| Theorem | nmosetre 30783* | The set in the supremum of the operator norm definition df-nmoo 30764 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ) | ||
| Theorem | nmosetn0 30784* | The set in the supremum of the operator norm definition df-nmoo 30764 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))}) | ||
| Theorem | nmoxr 30785 | The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) ∈ ℝ*) | ||
| Theorem | nmooge0 30786 | The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → 0 ≤ (𝑁‘𝑇)) | ||
| Theorem | nmorepnf 30787 | The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) ≠ +∞)) | ||
| Theorem | nmoreltpnf 30788 | The norm of any operator is real iff it is less than plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) < +∞)) | ||
| Theorem | nmogtmnf 30789 | The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → -∞ < (𝑁‘𝑇)) | ||
| Theorem | nmoolb 30790 | A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ (𝑁‘𝑇)) | ||
| Theorem | nmoubi 30791* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ*) → ((𝑁‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
| Theorem | nmoub3i 30792* | An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) | ||
| Theorem | nmoub2i 30793* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) | ||
| Theorem | nmobndi 30794* | Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) ∈ ℝ ↔ ∃𝑟 ∈ ℝ ∀𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 → (𝑀‘(𝑇‘𝑦)) ≤ 𝑟))) | ||
| Theorem | nmounbi 30795* | Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) = +∞ ↔ ∀𝑟 ∈ ℝ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑟 < (𝑀‘(𝑇‘𝑦))))) | ||
| Theorem | nmounbseqi 30796* | An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
| Theorem | nmounbseqiALT 30797* | Alternate shorter proof of nmounbseqi 30796 based on Axioms ax-reg 9632 and ax-ac2 10503 instead of ax-cc 10475. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
| Theorem | nmobndseqi 30798* | A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
| Theorem | nmobndseqiALT 30799* | Alternate shorter proof of nmobndseqi 30798 based on Axioms ax-reg 9632 and ax-ac2 10503 instead of ax-cc 10475. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
| Theorem | bloval 30800* | The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐵 = {𝑡 ∈ 𝐿 ∣ (𝑁‘𝑡) < +∞}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |