HomeTheorem List (p. 322 of 507)
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. 322 of 507) | < 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-31307) |
Hilbert Space Explorer
(31308-32830) |
Users' Mathboxes
(32831-50694) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pjdsi 32101 | Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ (𝐺 ∨ℋ 𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻)) → 𝐴 = (((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pjds3i 32102 | Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (((𝐴 ∈ ((𝐹 ∨ℋ 𝐺) ∨ℋ 𝐻) ∧ 𝐹 ⊆ (⊥‘𝐺)) ∧ (𝐹 ⊆ (⊥‘𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻))) → 𝐴 = ((((projℎ‘𝐹)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)) +ℎ ((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pj11 32103 | One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)) | ||
| Theorem | pjmfn 32104 | Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ projℎ Fn Cℋ | ||
| Theorem | pjmf1 32105 | The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ projℎ: Cℋ –1-1→( ℋ ↑m ℋ) | ||
| Theorem | pjoi0 32106 | The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
| ⊢ (((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) ∧ 𝐺 ⊆ (⊥‘𝐻)) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0) | ||
| Theorem | pjoi0i 32107 | The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐺 ⊆ (⊥‘𝐻) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0) | ||
| Theorem | pjopythi 32108 | Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐺 ⊆ (⊥‘𝐻) → ((normℎ‘(((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐺)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2))) | ||
| Theorem | pjopyth 32109 | Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐺)‘𝐴))↑2)))) | ||
| Theorem | pjnormi 32110 | The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘𝐴) | ||
| Theorem | pjpythi 32111 | Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴)↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘(⊥‘𝐻))‘𝐴))↑2)) | ||
| Theorem | pjneli 32112 | If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (¬ 𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) < (normℎ‘𝐴)) | ||
| Theorem | pjnorm 32113 | The norm of the projection is less than or equal to the norm. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘𝐴)) | ||
| Theorem | pjpyth 32114 | Pythagorean theorem for projectors. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((normℎ‘𝐴)↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘(⊥‘𝐻))‘𝐴))↑2))) | ||
| Theorem | pjnel 32115 | If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (¬ 𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) < (normℎ‘𝐴))) | ||
| Theorem | pjnorm2 32116 | A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 32083 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) = (normℎ‘𝐴))) | ||
| Theorem | mayete3i 32117 | Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐴 ⊆ (⊥‘𝐶) & ⊢ 𝐴 ⊆ (⊥‘𝐹) & ⊢ 𝐶 ⊆ (⊥‘𝐹) & ⊢ 𝐴 ⊆ (⊥‘𝐵) & ⊢ 𝐶 ⊆ (⊥‘𝐷) & ⊢ 𝐹 ⊆ (⊥‘𝐺) & ⊢ 𝑋 = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) & ⊢ 𝑌 = (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺)) & ⊢ 𝑍 = ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ⇒ ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑍 | ||
| Theorem | mayetes3i 32118 | Mayet's equation E^*3, derived from E3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. (Contributed by NM, 10-May-2009.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝐴 ⊆ (⊥‘𝐶) & ⊢ 𝐴 ⊆ (⊥‘𝐹) & ⊢ 𝐶 ⊆ (⊥‘𝐹) & ⊢ 𝐴 ⊆ (⊥‘𝐵) & ⊢ 𝐶 ⊆ (⊥‘𝐷) & ⊢ 𝐹 ⊆ (⊥‘𝐺) & ⊢ 𝑅 ⊆ (⊥‘𝑋) & ⊢ 𝑋 = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) & ⊢ 𝑌 = (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺)) & ⊢ 𝑍 = ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ⇒ ⊢ ((𝑋 ∨ℋ 𝑅) ∩ 𝑌) ⊆ (𝑍 ∨ℋ 𝑅) | ||
Note on operators. Unlike some authors, we use the term "operator" to mean any function from ℋ to ℋ. This is the definition of operator in [Hughes] p. 14, the definition of operator in [AkhiezerGlazman] p. 30, and the definition of operator in [Goldberg] p. 10. For Reed and Simon, an operator is linear (definition of operator in [ReedSimon] p. 2). For Halmos, an operator is bounded and linear (definition of operator in [Halmos] p. 35). For Kalmbach and Beran, an operator is continuous and linear (definition of operator in [Kalmbach] p. 353; definition of operator in [Beran] p. 99). Note that "bounded and linear" and "continuous and linear" are equivalent by lncnbd 32427. | ||
| Definition | df-hosum 32119* | Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
| ⊢ +op = (𝑓 ∈ ( ℋ ↑m ℋ), 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) +ℎ (𝑔‘𝑥)))) | ||
| Definition | df-homul 32120* | Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ ·op = (𝑓 ∈ ℂ, 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 ·ℎ (𝑔‘𝑥)))) | ||
| Definition | df-hodif 32121* | Define the difference of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
| ⊢ −op = (𝑓 ∈ ( ℋ ↑m ℋ), 𝑔 ∈ ( ℋ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) −ℎ (𝑔‘𝑥)))) | ||
| Definition | df-hfsum 32122* | Define the sum of two Hilbert space functionals. Definition of [Beran] p. 111. Note that unlike some authors, we define a functional as any function from ℋ to ℂ, not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ +fn = (𝑓 ∈ (ℂ ↑m ℋ), 𝑔 ∈ (ℂ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) + (𝑔‘𝑥)))) | ||
| Definition | df-hfmul 32123* | Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
| ⊢ ·fn = (𝑓 ∈ ℂ, 𝑔 ∈ (ℂ ↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 · (𝑔‘𝑥)))) | ||
| Theorem | hosmval 32124* | Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) +ℎ (𝑇‘𝑥)))) | ||
| Theorem | hommval 32125* | Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇) = (𝑥 ∈ ℋ ↦ (𝐴 ·ℎ (𝑇‘𝑥)))) | ||
| Theorem | hodmval 32126* | Value of the difference of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) −ℎ (𝑇‘𝑥)))) | ||
| Theorem | hfsmval 32127* | Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ℂ ∧ 𝑇: ℋ⟶ℂ) → (𝑆 +fn 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) + (𝑇‘𝑥)))) | ||
| Theorem | hfmmval 32128* | Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ℂ) → (𝐴 ·fn 𝑇) = (𝑥 ∈ ℋ ↦ (𝐴 · (𝑇‘𝑥)))) | ||
| Theorem | hosval 32129 | Value of the sum of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) = ((𝑆‘𝐴) +ℎ (𝑇‘𝐴))) | ||
| Theorem | homval 32130 | Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) = (𝐴 ·ℎ (𝑇‘𝐵))) | ||
| Theorem | hodval 32131 | Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) = ((𝑆‘𝐴) −ℎ (𝑇‘𝐴))) | ||
| Theorem | hfsval 32132 | Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ℂ ∧ 𝑇: ℋ⟶ℂ ∧ 𝐴 ∈ ℋ) → ((𝑆 +fn 𝑇)‘𝐴) = ((𝑆‘𝐴) + (𝑇‘𝐴))) | ||
| Theorem | hfmval 32133 | Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·fn 𝑇)‘𝐵) = (𝐴 · (𝑇‘𝐵))) | ||
| Theorem | hoscl 32134 | Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | homcl 32135 | Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) ∈ ℋ) | ||
| Theorem | hodcl 32136 | Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ) | ||
| Definition | df-h0op 32137 | Define the Hilbert space zero operator. See df0op2 32141 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop = (projℎ‘0ℋ) | ||
| Definition | df-iop 32138 | Define the Hilbert space identity operator. See dfiop2 32142 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ Iop = (projℎ‘ ℋ) | ||
| Theorem | ho0val 32139 | Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ( 0hop ‘𝐴) = 0ℎ) | ||
| Theorem | ho0f 32140 | Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 0hop : ℋ⟶ ℋ | ||
| Theorem | df0op2 32141 | Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ 0hop = ( ℋ × 0ℋ) | ||
| Theorem | dfiop2 32142 | Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop = ( I ↾ ℋ) | ||
| Theorem | hoif 32143 | Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop : ℋ–1-1-onto→ ℋ | ||
| Theorem | hoival 32144 | The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ( Iop ‘𝐴) = 𝐴) | ||
| Theorem | hoico1 32145 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∘ Iop ) = 𝑇) | ||
| Theorem | hoico2 32146 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ( Iop ∘ 𝑇) = 𝑇) | ||
| Theorem | hoaddcl 32147 | The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇): ℋ⟶ ℋ) | ||
| Theorem | homulcl 32148 | The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op 𝑇): ℋ⟶ ℋ) | ||
| Theorem | hoeq 32149* | Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑈‘𝑥) ↔ 𝑇 = 𝑈)) | ||
| Theorem | hoeqi 32150* | Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇) | ||
| Theorem | hoscli 32151 | Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hodcli 32152 | Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hocoi 32153 | Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴))) | ||
| Theorem | hococli 32154 | Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hocofi 32155 | Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 ∘ 𝑇): ℋ⟶ ℋ | ||
| Theorem | hocofni 32156 | Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 ∘ 𝑇) Fn ℋ | ||
| Theorem | hoaddcli 32157 | Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇): ℋ⟶ ℋ | ||
| Theorem | hosubcli 32158 | Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇): ℋ⟶ ℋ | ||
| Theorem | hoaddfni 32159 | Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) Fn ℋ | ||
| Theorem | hosubfni 32160 | Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇) Fn ℋ | ||
| Theorem | hoaddcomi 32161 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) = (𝑇 +op 𝑆) | ||
| Theorem | hosubcl 32162 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇): ℋ⟶ ℋ) | ||
| Theorem | hoaddcom 32163 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑇 +op 𝑆)) | ||
| Theorem | hodsi 32164 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) = 𝑇 ↔ (𝑆 +op 𝑇) = 𝑅) | ||
| Theorem | hoaddassi 32165 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)) | ||
| Theorem | hoadd12i 32166 | Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑅 +op (𝑆 +op 𝑇)) = (𝑆 +op (𝑅 +op 𝑇)) | ||
| Theorem | hoadd32i 32167 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) +op 𝑇) = ((𝑅 +op 𝑇) +op 𝑆) | ||
| Theorem | hocadddiri 32168 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) +op (𝑆 ∘ 𝑇)) | ||
| Theorem | hocsubdiri 32169 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇)) | ||
| Theorem | ho2coi 32170 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((𝑅 ∘ 𝑆) ∘ 𝑇)‘𝐴) = (𝑅‘(𝑆‘(𝑇‘𝐴)))) | ||
| Theorem | hoaddass 32171 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇))) | ||
| Theorem | hoadd32 32172 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = ((𝑅 +op 𝑇) +op 𝑆)) | ||
| Theorem | hoadd4 32173 | Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) +op (𝑇 +op 𝑈)) = ((𝑅 +op 𝑇) +op (𝑆 +op 𝑈))) | ||
| Theorem | hocsubdir 32174 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇))) | ||
| Theorem | hoaddridi 32175 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 0hop ) = 𝑇 | ||
| Theorem | hodidi 32176 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 −op 𝑇) = 0hop | ||
| Theorem | ho0coi 32177 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( 0hop ∘ 𝑇) = 0hop | ||
| Theorem | hoid1i 32178 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 ∘ Iop ) = 𝑇 | ||
| Theorem | hoid1ri 32179 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( Iop ∘ 𝑇) = 𝑇 | ||
| Theorem | hoaddrid 32180 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 +op 0hop ) = 𝑇) | ||
| Theorem | hodid 32181 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 𝑇) = 0hop ) | ||
| Theorem | hon0 32182 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ¬ 𝑇 = ∅) | ||
| Theorem | hodseqi 32183 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (𝑇 −op 𝑆)) = 𝑇 | ||
| Theorem | ho0subi 32184 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇)) | ||
| Theorem | honegsubi 32185 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (-1 ·op 𝑇)) = (𝑆 −op 𝑇) | ||
| Theorem | ho0sub 32186 | Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇) = (𝑆 +op ( 0hop −op 𝑇))) | ||
| Theorem | hosubid1 32187 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇) | ||
| Theorem | honegsub 32188 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op (-1 ·op 𝑈)) = (𝑇 −op 𝑈)) | ||
| Theorem | homullid 32189 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇) | ||
| Theorem | homco1 32190 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
| Theorem | homulass 32191 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))) | ||
| Theorem | hoadddi 32192 | Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op 𝑈))) | ||
| Theorem | hoadddir 32193 | Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op 𝑇))) | ||
| Theorem | homul12 32194 | Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)) = (𝐵 ·op (𝐴 ·op 𝑇))) | ||
| Theorem | honegneg 32195 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇) | ||
| Theorem | hosubneg 32196 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈)) | ||
| Theorem | hosubdi 32197 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈))) | ||
| Theorem | honegdi 32198 | Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 +op 𝑈)) = ((-1 ·op 𝑇) +op (-1 ·op 𝑈))) | ||
| Theorem | honegsubdi 32199 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈)) | ||
| Theorem | honegsubdi2 32200 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |