HomeTheorem List (p. 280 of 424)
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. 280 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 5oalem5 27901 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-May-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ (𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆))) ∧ (((𝑥 +ℎ 𝑦) = (𝑣 +ℎ 𝑢) ∧ (𝑧 +ℎ 𝑤) = (𝑣 +ℎ 𝑢)) ∧ (𝑓 +ℎ 𝑔) = (𝑣 +ℎ 𝑢))) → (𝑥 −ℎ 𝑧) ∈ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))) | ||
| Theorem | 5oalem6 27902 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ℎ = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷) ∧ ℎ = (𝑧 +ℎ 𝑤))) ∧ (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ ℎ = (𝑓 +ℎ 𝑔)) ∧ ((𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆) ∧ ℎ = (𝑣 +ℎ 𝑢)))) → ℎ ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))) | ||
| Theorem | 5oalem7 27903 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))))) | ||
| Theorem | 5oai 27904 | Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ & ⊢ 𝐴 ⊆ (⊥‘𝐵) & ⊢ 𝐶 ⊆ (⊥‘𝐷) & ⊢ 𝐹 ⊆ (⊥‘𝐺) & ⊢ 𝑅 ⊆ (⊥‘𝑆) ⇒ ⊢ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ ((𝐹 ∨ℋ 𝐺) ∩ (𝑅 ∨ℋ 𝑆))) ⊆ (𝐵 ∨ℋ (𝐴 ∩ (𝐶 ∨ℋ ((((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐷)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)))) ∩ ((((𝐴 ∨ℋ 𝐹) ∩ (𝐵 ∨ℋ 𝐺)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆)))) ∨ℋ (((𝐶 ∨ℋ 𝐹) ∩ (𝐷 ∨ℋ 𝐺)) ∩ (((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆))))))))) | ||
| Theorem | 3oalem1 27905* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ))) | ||
| Theorem | 3oalem2 27906* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) | ||
| Theorem | 3oalem3 27907 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) | ||
| Theorem | 3oalem4 27908 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) ⇒ ⊢ 𝑅 ⊆ (⊥‘𝐵) | ||
| Theorem | 3oalem5 27909 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) | ||
| Theorem | 3oalem6 27910 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆))))) | ||
| Theorem | 3oai 27911 | 3OA (weak) orthoarguesian law. Equation IV of [GodowskiGreechie] p. 249. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆))))) | ||
| Theorem | pjorthi 27912 | Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0) | ||
| Theorem | pjch1 27913 | Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴) | ||
| Theorem | pjo 27914 | The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pjcompi 27915 | Component of a projection. (Contributed by NM, 31-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴) | ||
| Theorem | pjidmi 27916 | A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘((projℎ‘𝐻)‘𝐴)) = ((projℎ‘𝐻)‘𝐴) | ||
| Theorem | pjadjii 27917 | A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵)) | ||
| Theorem | pjaddii 27918 | Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) | ||
| Theorem | pjinormii 27919 | The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) | ||
| Theorem | pjmulii 27920 | Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjsubii 27921 | Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)) | ||
| Theorem | pjsslem 27922 | Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjss2i 27923 | Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (𝐻 ⊆ 𝐺 → ((projℎ‘𝐻)‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjssmii 27924 | Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)) | ||
| Theorem | pjssge0ii 27925 | Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴)) | ||
| Theorem | pjdifnormii 27926 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴))) | ||
| Theorem | pjcji 27927 | The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴))) | ||
| Theorem | pjadji 27928 | A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjaddi 27929 | Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjinormi 27930 | The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2)) | ||
| Theorem | pjsubi 27931 | Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjmuli 27932 | Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjige0i 27933 | The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴)) | ||
| Theorem | pjige0 27934 | The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴)) | ||
| Theorem | pjcjt2 27935 | The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))) | ||
| Theorem | pj0i 27936 | The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ | ||
| Theorem | pjch 27937 | Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ ((projℎ‘𝐻)‘𝐴) = 𝐴)) | ||
| Theorem | pjid 27938 | The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻) → ((projℎ‘𝐻)‘𝐴) = 𝐴) | ||
| Theorem | pjvec 27939* | The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → 𝐻 = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 𝑥}) | ||
| Theorem | pjocvec 27940* | The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (⊥‘𝐻) = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 0ℎ}) | ||
| Theorem | pjocini 27941 | Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻))) | ||
| Theorem | pjini 27942 | Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻)) | ||
| Theorem | pjjsi 27943* | A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ (∀𝑥 ∈ (𝐺 ∨ℋ 𝐻)((projℎ‘(⊥‘𝐺))‘𝑥) ∈ 𝐻 → (𝐺 ∨ℋ 𝐻) = (𝐺 +ℋ 𝐻)) | ||
| Theorem | pjfni 27944 | Functionality of a projection. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻) Fn ℋ | ||
| Theorem | pjrni 27945 | The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ran (projℎ‘𝐻) = 𝐻 | ||
| Theorem | pjfoi 27946 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻): ℋ–onto→𝐻 | ||
| Theorem | pjfi 27947 | The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻): ℋ⟶ ℋ | ||
| Theorem | pjvi 27948 | The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴) | ||
| Theorem | pjhfo 27949 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ–onto→𝐻) | ||
| Theorem | pjrn 27950 | The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → ran (projℎ‘𝐻) = 𝐻) | ||
| Theorem | pjhf 27951 | The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ⟶ ℋ) | ||
| Theorem | pjfn 27952 | Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) Fn ℋ) | ||
| Theorem | pjsumi 27953 | The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → (𝐺 ⊆ (⊥‘𝐻) → ((projℎ‘(𝐺 +ℋ 𝐻))‘𝐴) = (((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))) | ||
| Theorem | pj11i 27954 | One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻) | ||
| Theorem | pjdsi 27955 | 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 27956 | 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 27957 | One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)) | ||
| Theorem | pjmfn 27958 | Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ projℎ Fn Cℋ | ||
| Theorem | pjmf1 27959 | 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→( ℋ ↑𝑚 ℋ) | ||
| Theorem | pjoi0 27960 | 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 27961 | 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 27962 | 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 27963 | 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 27964 | 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 27965 | 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 27966 | 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 27967 | 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 27968 | 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 27969 | 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 27970 | A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 27937 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) = (normℎ‘𝐴))) | ||
| Theorem | mayete3i 27971 | 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 27972 | 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 28281. | ||
| Definition | df-hosum 27973* | Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
| ⊢ +op = (𝑓 ∈ ( ℋ ↑𝑚 ℋ), 𝑔 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) +ℎ (𝑔‘𝑥)))) | ||
| Definition | df-homul 27974* | 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 = (𝑓 ∈ ℂ, 𝑔 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 ·ℎ (𝑔‘𝑥)))) | ||
| Definition | df-hodif 27975* | Define the difference of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
| ⊢ −op = (𝑓 ∈ ( ℋ ↑𝑚 ℋ), 𝑔 ∈ ( ℋ ↑𝑚 ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) −ℎ (𝑔‘𝑥)))) | ||
| Definition | df-hfsum 27976* | 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 = (𝑓 ∈ (ℂ ↑𝑚 ℋ), 𝑔 ∈ (ℂ ↑𝑚 ℋ) ↦ (𝑥 ∈ ℋ ↦ ((𝑓‘𝑥) + (𝑔‘𝑥)))) | ||
| Definition | df-hfmul 27977* | 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 = (𝑓 ∈ ℂ, 𝑔 ∈ (ℂ ↑𝑚 ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 · (𝑔‘𝑥)))) | ||
| Theorem | hosmval 27978* | 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 27979* | 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 27980* | 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 27981* | 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 27982* | 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 27983 | 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 27984 | 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 27985 | 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 27986 | 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 27987 | 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 27988 | Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 +op 𝑇)‘𝐴) ∈ ℋ) | ||
| Theorem | homcl 27989 | Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·op 𝑇)‘𝐵) ∈ ℋ) | ||
| Theorem | hodcl 27990 | Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.) |
| ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝐴 ∈ ℋ) → ((𝑆 −op 𝑇)‘𝐴) ∈ ℋ) | ||
| Definition | df-h0op 27991 | Define the Hilbert space zero operator. See df0op2 27995 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
| ⊢ 0hop = (projℎ‘0ℋ) | ||
| Definition | df-iop 27992 | Define the Hilbert space identity operator. See dfiop2 27996 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
| ⊢ Iop = (projℎ‘ ℋ) | ||
| Theorem | ho0val 27993 | 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 27994 | Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
| ⊢ 0hop : ℋ⟶ ℋ | ||
| Theorem | df0op2 27995 | Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ 0hop = ( ℋ × 0ℋ) | ||
| Theorem | dfiop2 27996 | Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop = ( I ↾ ℋ) | ||
| Theorem | hoif 27997 | Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ Iop : ℋ–1-1-onto→ ℋ | ||
| Theorem | hoival 27998 | The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ( Iop ‘𝐴) = 𝐴) | ||
| Theorem | hoico1 27999 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → (𝑇 ∘ Iop ) = 𝑇) | ||
| Theorem | hoico2 28000 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
| ⊢ (𝑇: ℋ⟶ ℋ → ( Iop ∘ 𝑇) = 𝑇) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |