HomeTheorem List (p. 318 of 499)
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. 318 of 499) | < 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-30893) |
Hilbert Space Explorer
(30894-32416) |
Users' Mathboxes
(32417-49836) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pjnel 31701 | 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 31702 | A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 31669 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) = (normℎ‘𝐴))) | ||
| Theorem | mayete3i 31703 | 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 31704 | 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 32013. | ||
| Definition | df-hosum 31705* | 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 31706* | 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 31707* | 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 31708* | 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 31709* | 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 31710* | 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 31711* | 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 31712* | 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 31713* | 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 31714* | 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 31715 | 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 31716 | 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 31717 | 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 31718 | 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 31719 | 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 31720 | Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | homcl 31721 | Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) ∈ ℋ) | ||
| Theorem | hodcl 31722 | Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ) | ||
| Definition | df-h0op 31723 | Define the Hilbert space zero operator. See df0op2 31727 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop = (projℎ‘0ℋ) | ||
| Definition | df-iop 31724 | Define the Hilbert space identity operator. See dfiop2 31728 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ Iop = (projℎ‘ ℋ) | ||
| Theorem | ho0val 31725 | 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 31726 | Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 0hop : ℋ⟶ ℋ | ||
| Theorem | df0op2 31727 | Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ 0hop = ( ℋ × 0ℋ) | ||
| Theorem | dfiop2 31728 | Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop = ( I ↾ ℋ) | ||
| Theorem | hoif 31729 | Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop : ℋ–1-1-onto→ ℋ | ||
| Theorem | hoival 31730 | The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ( Iop ‘𝐴) = 𝐴) | ||
| Theorem | hoico1 31731 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∘ Iop ) = 𝑇) | ||
| Theorem | hoico2 31732 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ( Iop ∘ 𝑇) = 𝑇) | ||
| Theorem | hoaddcl 31733 | 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 31734 | 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 31735* | Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (𝑇‘𝑥) = (𝑈‘𝑥) ↔ 𝑇 = 𝑈)) | ||
| Theorem | hoeqi 31736* | Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇) | ||
| Theorem | hoscli 31737 | Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hodcli 31738 | Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hocoi 31739 | Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) = (𝑆‘(𝑇‘𝐴))) | ||
| Theorem | hococli 31740 | Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | hocofi 31741 | Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 ∘ 𝑇): ℋ⟶ ℋ | ||
| Theorem | hocofni 31742 | Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 ∘ 𝑇) Fn ℋ | ||
| Theorem | hoaddcli 31743 | Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇): ℋ⟶ ℋ | ||
| Theorem | hosubcli 31744 | 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 31745 | Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) Fn ℋ | ||
| Theorem | hosubfni 31746 | Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 −op 𝑇) Fn ℋ | ||
| Theorem | hoaddcomi 31747 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op 𝑇) = (𝑇 +op 𝑆) | ||
| Theorem | hosubcl 31748 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 −op 𝑇): ℋ⟶ ℋ) | ||
| Theorem | hoaddcom 31749 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (𝑆 +op 𝑇) = (𝑇 +op 𝑆)) | ||
| Theorem | hodsi 31750 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) = 𝑇 ↔ (𝑆 +op 𝑇) = 𝑅) | ||
| Theorem | hoaddassi 31751 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇)) | ||
| Theorem | hoadd12i 31752 | 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 31753 | 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 31754 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) +op (𝑆 ∘ 𝑇)) | ||
| Theorem | hocsubdiri 31755 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇)) | ||
| Theorem | ho2coi 31756 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((𝑅 ∘ 𝑆) ∘ 𝑇)‘𝐴) = (𝑅‘(𝑆‘(𝑇‘𝐴)))) | ||
| Theorem | hoaddass 31757 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 +op 𝑆) +op 𝑇) = (𝑅 +op (𝑆 +op 𝑇))) | ||
| Theorem | hoadd32 31758 | 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 31759 | 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 31760 | Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → ((𝑅 −op 𝑆) ∘ 𝑇) = ((𝑅 ∘ 𝑇) −op (𝑆 ∘ 𝑇))) | ||
| Theorem | hoaddridi 31761 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 0hop ) = 𝑇 | ||
| Theorem | hodidi 31762 | Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 −op 𝑇) = 0hop | ||
| Theorem | ho0coi 31763 | Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( 0hop ∘ 𝑇) = 0hop | ||
| Theorem | hoid1i 31764 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑇 ∘ Iop ) = 𝑇 | ||
| Theorem | hoid1ri 31765 | Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ( Iop ∘ 𝑇) = 𝑇 | ||
| Theorem | hoaddrid 31766 | Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 +op 0hop ) = 𝑇) | ||
| Theorem | hodid 31767 | Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 𝑇) = 0hop ) | ||
| Theorem | hon0 31768 | A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ¬ 𝑇 = ∅) | ||
| Theorem | hodseqi 31769 | Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (𝑇 −op 𝑆)) = 𝑇 | ||
| Theorem | ho0subi 31770 | 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 31771 | Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝑆 +op (-1 ·op 𝑇)) = (𝑆 −op 𝑇) | ||
| Theorem | ho0sub 31772 | 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 31773 | The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 −op 0hop ) = 𝑇) | ||
| Theorem | honegsub 31774 | Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +op (-1 ·op 𝑈)) = (𝑇 −op 𝑈)) | ||
| Theorem | homullid 31775 | An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇) | ||
| Theorem | homco1 31776 | Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈))) | ||
| Theorem | homulass 31777 | Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))) | ||
| Theorem | hoadddi 31778 | 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 31779 | 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 31780 | 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 31781 | Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (-1 ·op (-1 ·op 𝑇)) = 𝑇) | ||
| Theorem | hosubneg 31782 | Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 −op (-1 ·op 𝑈)) = (𝑇 +op 𝑈)) | ||
| Theorem | hosubdi 31783 | Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝐴 ·op (𝑇 −op 𝑈)) = ((𝐴 ·op 𝑇) −op (𝐴 ·op 𝑈))) | ||
| Theorem | honegdi 31784 | 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 31785 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = ((-1 ·op 𝑇) +op 𝑈)) | ||
| Theorem | honegsubdi2 31786 | Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (-1 ·op (𝑇 −op 𝑈)) = (𝑈 −op 𝑇)) | ||
| Theorem | hosubsub2 31787 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = (𝑆 +op (𝑈 −op 𝑇))) | ||
| Theorem | hosub4 31788 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 +op 𝑆) −op (𝑇 +op 𝑈)) = ((𝑅 −op 𝑇) +op (𝑆 −op 𝑈))) | ||
| Theorem | hosubadd4 31789 | Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (((𝑅: ℋ⟶ ℋ ∧ 𝑆: ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ)) → ((𝑅 −op 𝑆) −op (𝑇 −op 𝑈)) = ((𝑅 +op 𝑈) −op (𝑆 +op 𝑇))) | ||
| Theorem | hoaddsubass 31790 | Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = (𝑆 +op (𝑇 −op 𝑈))) | ||
| Theorem | hoaddsub 31791 | Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 +op 𝑇) −op 𝑈) = ((𝑆 −op 𝑈) +op 𝑇)) | ||
| Theorem | hosubsub 31792 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑆 −op (𝑇 −op 𝑈)) = ((𝑆 −op 𝑇) +op 𝑈)) | ||
| Theorem | hosubsub4 31793 | Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.) |
| ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → ((𝑆 −op 𝑇) −op 𝑈) = (𝑆 −op (𝑇 +op 𝑈))) | ||
| Theorem | ho2times 31794 | Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (2 ·op 𝑇) = (𝑇 +op 𝑇)) | ||
| Theorem | hoaddsubassi 31795 | Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = (𝑅 +op (𝑆 −op 𝑇)) | ||
| Theorem | hoaddsubi 31796 | Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑅: ℋ⟶ ℋ & ⊢ 𝑆: ℋ⟶ ℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ ((𝑅 +op 𝑆) −op 𝑇) = ((𝑅 −op 𝑇) +op 𝑆) | ||
| Theorem | hosd1i 31797 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ( 0hop −op 𝑈)) | ||
| Theorem | hosd2i 31798 | Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ (𝑇 +op 𝑈) = (𝑇 −op ((𝑈 −op 𝑈) −op 𝑈)) | ||
| Theorem | hopncani 31799 | Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 +op 𝑈) −op 𝑈) = 𝑇 | ||
| Theorem | honpcani 31800 | Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ 𝑇: ℋ⟶ ℋ & ⊢ 𝑈: ℋ⟶ ℋ ⇒ ⊢ ((𝑇 −op 𝑈) +op 𝑈) = 𝑇 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |