HomeTheorem List (p. 317 of 498)
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. 317 of 498) | < 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-30880) |
Hilbert Space Explorer
(30881-32403) |
Users' Mathboxes
(32404-49791) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | chscllem3 31601* | Lemma for chscl 31603. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁)) | ||
| Theorem | chscllem4 31602* | Lemma for chscl 31603. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛))) ⇒ ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵)) | ||
| Theorem | chscl 31603 | The subspace sum of two closed orthogonal spaces is closed. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) ⇒ ⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Cℋ ) | ||
| Theorem | osumi 31604 | If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the (countable) Axiom of Choice is used for this proof via pjhth 31355, although "the hard part" of this proof, chscl 31603, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | osumcori 31605 | Corollary of osumi 31604. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))) | ||
| Theorem | osumcor2i 31606 | Corollary of osumi 31604, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | osum 31607 | If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | spansnji 31608 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵})) | ||
| Theorem | spansnj 31609 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵}))) | ||
| Theorem | spansnscl 31610 | The subspace sum of a closed subspace and a one-dimensional subspace is closed. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) ∈ Cℋ ) | ||
| Theorem | sumspansn 31611 | The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ∈ (span‘{𝐴}) ↔ 𝐵 ∈ (span‘{𝐴}))) | ||
| Theorem | spansnm0i 31612 | The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (¬ 𝐴 ∈ (span‘{𝐵}) → ((span‘{𝐴}) ∩ (span‘{𝐵})) = 0ℋ) | ||
| Theorem | nonbooli 31613 | A Hilbert lattice with two or more dimensions fails the distributive law and therefore cannot be a Boolean algebra. This counterexample demonstrates a condition where ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺)) = 0ℋ but (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ 0ℋ. The antecedent specifies that the vectors 𝐴 and 𝐵 are nonzero and non-colinear. The last three hypotheses assign one-dimensional subspaces to 𝐹, 𝐺, and 𝐻. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐹 = (span‘{𝐴}) & ⊢ 𝐺 = (span‘{𝐵}) & ⊢ 𝐻 = (span‘{(𝐴 +ℎ 𝐵)}) ⇒ ⊢ (¬ (𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹) → (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺))) | ||
| Theorem | spansncvi 31614 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶}))) | ||
| Theorem | spansncv 31615 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶})))) | ||
| Theorem | 5oalem1 31616 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ ⇒ ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅)))) | ||
| Theorem | 5oalem2 31617 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ ⇒ ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷))) | ||
| Theorem | 5oalem3 31618 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))) | ||
| Theorem | 5oalem4 31619 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))) | ||
| Theorem | 5oalem5 31620 | 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 31621 | 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 31622 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2349 with 4exdistrv 1956 as in 3oalem3 31626. (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))))) | ||
| Theorem | 5oai 31623 | 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 31624* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ))) | ||
| Theorem | 3oalem2 31625* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) | ||
| Theorem | 3oalem3 31626 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) | ||
| Theorem | 3oalem4 31627 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) ⇒ ⊢ 𝑅 ⊆ (⊥‘𝐵) | ||
| Theorem | 3oalem5 31628 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) | ||
| Theorem | 3oalem6 31629 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆))))) | ||
| Theorem | 3oai 31630 | 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 31631 | Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0) | ||
| Theorem | pjch1 31632 | Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴) | ||
| Theorem | pjo 31633 | 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 31634 | 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 31635 | 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 31636 | 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 31637 | Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) | ||
| Theorem | pjinormii 31638 | 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 31639 | Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjsubii 31640 | Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)) | ||
| Theorem | pjsslem 31641 | Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjss2i 31642 | 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 31643 | 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 31644 | 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 31645 | 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 31646 | 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 31647 | 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 31648 | Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjinormi 31649 | 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 31650 | Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjmuli 31651 | Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵))) | ||
| Theorem | pjige0i 31652 | 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 31653 | 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 31654 | 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 31655 | The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ | ||
| Theorem | pjch 31656 | 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 31657 | 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 31658* | 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 31659* | 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 31660 | Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻))) | ||
| Theorem | pjini 31661 | Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻)) | ||
| Theorem | pjjsi 31662* | 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 31663 | 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 31664 | 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 31665 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻): ℋ–onto→𝐻 | ||
| Theorem | pjfi 31666 | The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (projℎ‘𝐻): ℋ⟶ ℋ | ||
| Theorem | pjvi 31667 | The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴) | ||
| Theorem | pjhfo 31668 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ–onto→𝐻) | ||
| Theorem | pjrn 31669 | 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 31670 | The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ⟶ ℋ) | ||
| Theorem | pjfn 31671 | Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
| ⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) Fn ℋ) | ||
| Theorem | pjsumi 31672 | 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 31673 | One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻) | ||
| Theorem | pjdsi 31674 | 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 31675 | 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 31676 | One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)) | ||
| Theorem | pjmfn 31677 | Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ projℎ Fn Cℋ | ||
| Theorem | pjmf1 31678 | 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 31679 | 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 31680 | 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 31681 | 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 31682 | 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 31683 | 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 31684 | 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 31685 | 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 31686 | 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 31687 | 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 31688 | 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 31689 | A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 31656 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) = (normℎ‘𝐴))) | ||
| Theorem | mayete3i 31690 | 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 31691 | 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 32000. | ||
| Definition | df-hosum 31692* | 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 31693* | 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 31694* | 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 31695* | 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 31696* | 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 31697* | 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 31698* | 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 31699* | 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 31700* | 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 𝑇) = (𝑥 ∈ ℋ ↦ ((𝑆‘𝑥) + (𝑇‘𝑥)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |