HomeTheorem List (p. 300 of 476)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 300 of 476) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30098) |
Hilbert Space Explorer
(30099-31621) |
Users' Mathboxes
(31622-47564) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | css 29901 | Extend class notation with the class of all subspaces of normed complex vector spaces. |
| class SubSp | ||
| Definition | df-ssp 29902* | 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 29903* | 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 29904 | The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐹 = ( +𝑣 ‘𝑊) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁)))) | ||
| Theorem | sspid 29905 | A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻) | ||
| Theorem | sspnv 29906 | A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) | ||
| Theorem | sspba 29907 | 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 29908 | 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 29909 | 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 29910 | 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 29911 | 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 29912* | Lemma for sspm 29914 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) & ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) & ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅) & ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) | ||
| Theorem | sspmval 29913 | 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 29914 | 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 29915 | 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 29916 | 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 29917 | 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 29918 | 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 29919 | 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 29920 | Extend class notation with the class of linear operators on normed complex vector spaces. |
| class LnOp | ||
| Syntax | cnmoo 29921 | Extend class notation with the class of operator norms on normed complex vector spaces. |
| class normOpOLD | ||
| Syntax | cblo 29922 | Extend class notation with the class of bounded linear operators on normed complex vector spaces. |
| class BLnOp | ||
| Syntax | c0o 29923 | Extend class notation with the class of zero operators on normed complex vector spaces. |
| class 0op | ||
| Definition | df-lno 29924* | 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 29925* | 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 29926* | 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 29927* | 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 29928 | Adjoint of an operator. |
| class adj | ||
| Syntax | chmo 29929 | Set of Hermitional (self-adjoint) operators. |
| class HmOp | ||
| Definition | df-aj 29930* | 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 29931* | 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 29932* | 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 29933* | 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 29934 | 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 29935 | 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 29936 | 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 29937 | 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 29938 | 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 29939 | 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 29940 | 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 29941 | Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍})) | ||
| Theorem | nmoofval 29942* | 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 29943* | 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 29944* | The set in the supremum of the operator norm definition df-nmoo 29925 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ) | ||
| Theorem | nmosetn0 29945* | The set in the supremum of the operator norm definition df-nmoo 29925 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))}) | ||
| Theorem | nmoxr 29946 | 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 29947 | 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 29948 | 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 29949 | 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 29950 | 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 29951 | 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 29952* | 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 29953* | 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 29954* | 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 29955* | 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 29956* | 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 29957* | 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 29958* | Alternate shorter proof of nmounbseqi 29957 based on Axioms ax-reg 9571 and ax-ac2 10442 instead of ax-cc 10414. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
| Theorem | nmobndseqi 29959* | 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 29960* | Alternate shorter proof of nmobndseqi 29959 based on Axioms ax-reg 9571 and ax-ac2 10442 instead of ax-cc 10414. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
| Theorem | bloval 29961* | 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) → 𝐵 = {𝑡 ∈ 𝐿 ∣ (𝑁‘𝑡) < +∞}) | ||
| Theorem | isblo 29962 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞))) | ||
| Theorem | isblo2 29963 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ))) | ||
| Theorem | bloln 29964 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿) | ||
| Theorem | blof 29965 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌) | ||
| Theorem | nmblore 29966 | The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → (𝑁‘𝑇) ∈ ℝ) | ||
| Theorem | 0ofval 29967 | The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝑂 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑂 = (𝑋 × {𝑍})) | ||
| Theorem | 0oval 29968 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝑂 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍) | ||
| Theorem | 0oo 29969 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌) | ||
| Theorem | 0lno 29970 | The zero operator is linear. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐿) | ||
| Theorem | nmoo0 29971 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) | ||
| Theorem | 0blo 29972 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵) | ||
| Theorem | nmlno0lem 29973 | Lemma for nmlno0i 29974. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝑃 = (0vec‘𝑈) & ⊢ 𝑄 = (0vec‘𝑊) & ⊢ 𝐾 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) ⇒ ⊢ ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) | ||
| Theorem | nmlno0i 29974 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) | ||
| Theorem | nmlno0 29975 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) | ||
| Theorem | nmlnoubi 29976* | An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝐾 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑁‘𝑇) ≤ 𝐴) | ||
| Theorem | nmlnogt0 29977 | The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇 ≠ 𝑍 ↔ 0 < (𝑁‘𝑇))) | ||
| Theorem | lnon0 29978* | The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑂 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ 𝑇 ≠ 𝑂) → ∃𝑥 ∈ 𝑋 𝑥 ≠ 𝑍) | ||
| Theorem | nmblolbii 29979 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) | ||
| Theorem | nmblolbi 29980 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋) → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) | ||
| Theorem | isblo3i 29981* | The predicate "is a bounded linear operator." Definition 2.7-1 of [Kreyszig] p. 91. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)))) | ||
| Theorem | blo3i 29982* | Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝐴 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐵) | ||
| Theorem | blometi 29983 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → ((𝑇‘𝑃)𝐷(𝑇‘𝑄)) ≤ ((𝑁‘𝑇) · (𝑃𝐶𝑄))) | ||
| Theorem | blocnilem 29984 | Lemma for blocni 29985 and lnocni 29986. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) | ||
| Theorem | blocni 29985 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 ⇒ ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵) | ||
| Theorem | lnocni 29986 | If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | blocn 29987 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (𝑇 ∈ 𝐿 → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵)) | ||
| Theorem | blocn2 29988 | A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ajfval 29989* | The adjoint function. (Contributed by NM, 25-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑄 = (·𝑖OLD‘𝑊) & ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {⟨𝑡, 𝑠⟩ ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) | ||
| Theorem | hmoval 29990* | The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑡 ∈ dom 𝐴 ∣ (𝐴‘𝑡) = 𝑡}) | ||
| Theorem | ishmo 29991 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ dom 𝐴 ∧ (𝐴‘𝑇) = 𝑇))) | ||
| Syntax | ccphlo 29992 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
| class CPreHilOLD | ||
| Definition | df-ph 29993* | Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of [ReedSimon] p. 63. The vector operation is 𝑔, the scalar product is 𝑠, and the norm is 𝑛. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) | ||
| Theorem | phnv 29994 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec) | ||
| Theorem | phrel 29995 | The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ Rel CPreHilOLD | ||
| Theorem | phnvi 29996 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | isphg 29997* | The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, and the norm is 𝑁. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ CPreHilOLD ↔ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) | ||
| Theorem | phop 29998 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩) | ||
| Theorem | cncph 29999 | The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩ ⇒ ⊢ 𝑈 ∈ CPreHilOLD | ||
| Theorem | elimph 30000 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |