![]() |
Metamath
Proof Explorer Theorem List (p. 289 of 437) | < 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: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | shsleji 28801 | Subspace sum is smaller than Hilbert lattice join. Remark in [Kalmbach] p. 65. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | shjcomi 28802 | Commutative law for join in Sℋ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
Theorem | shsub1i 28803 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 +ℋ 𝐵) | ||
Theorem | shsub2i 28804 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ 𝐴 ⊆ (𝐵 +ℋ 𝐴) | ||
Theorem | shub1i 28805 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | shjcli 28806 | Closure of Cℋ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ | ||
Theorem | shjshcli 28807 | Sℋ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) ∈ Sℋ | ||
Theorem | shlessi 28808 | Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶)) | ||
Theorem | shlej1i 28809 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | shlej2i 28810 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
Theorem | shslej 28811 | Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | shincl 28812 | Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∩ 𝐵) ∈ Sℋ ) | ||
Theorem | shub1 28813 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | shub2 28814 | A subspace is a subset of its Hilbert lattice join with another. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 ∨ℋ 𝐴)) | ||
Theorem | shsidmi 28815 | Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐴) = 𝐴 | ||
Theorem | shslubi 28816 | The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 +ℋ 𝐵) ⊆ 𝐶) | ||
Theorem | shlesb1i 28817 | Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 +ℋ 𝐵) = 𝐵) | ||
Theorem | shsval2i 28818* | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) = ∩ {𝑥 ∈ Sℋ ∣ (𝐴 ∪ 𝐵) ⊆ 𝑥} | ||
Theorem | shsval3i 28819 | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) = (span‘(𝐴 ∪ 𝐵)) | ||
Theorem | shmodsi 28820 | The modular law holds for subspace sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 +ℋ 𝐵) ∩ 𝐶) ⊆ (𝐴 +ℋ (𝐵 ∩ 𝐶))) | ||
Theorem | shmodi 28821 | The modular law is implied by the closure of subspace sum. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ ⇒ ⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ 𝐶) → ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) ⊆ (𝐴 ∨ℋ (𝐵 ∩ 𝐶))) | ||
Theorem | pjhthlem1 28822* | Lemma for pjhth 28824. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ (𝜑 → 𝐴 ∈ ℋ) & ⊢ (𝜑 → 𝐵 ∈ 𝐻) & ⊢ (𝜑 → 𝐶 ∈ 𝐻) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐻 (normℎ‘(𝐴 −ℎ 𝐵)) ≤ (normℎ‘(𝐴 −ℎ 𝑥))) & ⊢ 𝑇 = (((𝐴 −ℎ 𝐵) ·ih 𝐶) / ((𝐶 ·ih 𝐶) + 1)) ⇒ ⊢ (𝜑 → ((𝐴 −ℎ 𝐵) ·ih 𝐶) = 0) | ||
Theorem | pjhthlem2 28823* | Lemma for pjhth 28824. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ (𝜑 → 𝐴 ∈ ℋ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦)) | ||
Theorem | pjhth 28824 | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → (𝐻 +ℋ (⊥‘𝐻)) = ℋ) | ||
Theorem | pjhtheu 28825* | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102. See pjhtheu2 28847 for the uniqueness of 𝑦. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ∃!𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦)) | ||
Definition | df-pjh 28826* | Define the projection function on a Hilbert space, as a mapping from the Hilbert lattice to a function on Hilbert space. Every closed subspace is associated with a unique projection function. Remark in [Kalmbach] p. 66, adopted as a definition. (projℎ‘𝐻)‘𝐴 is the projection of vector 𝐴 onto closed subspace 𝐻. Note that the range of projℎ is the set of all projection operators, so 𝑇 ∈ ran projℎ means that 𝑇 is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
⊢ projℎ = (ℎ ∈ Cℋ ↦ (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ ℎ ∃𝑦 ∈ (⊥‘ℎ)𝑥 = (𝑧 +ℎ 𝑦)))) | ||
Theorem | pjhfval 28827* | The value of the projection map. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) = (𝑥 ∈ ℋ ↦ (℩𝑧 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝑥 = (𝑧 +ℎ 𝑦)))) | ||
Theorem | pjhval 28828* | Value of a projection. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (℩𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))) | ||
Theorem | pjpreeq 28829* | Equality with a projection. This version of pjeq 28830 does not assume the Axiom of Choice via pjhth 28824. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)))) | ||
Theorem | pjeq 28830* | Equality with a projection. (Contributed by NM, 20-Jan-2007.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)))) | ||
Theorem | axpjcl 28831 | Closure of a projection in its subspace. If we consider this together with axpjpj 28851 to be axioms, the need for the ax-hcompl 28631 can often be avoided for the kinds of theorems we are interested in here. An interesting project is to see how far we can go by using them in place of it. In particular, we can prove the orthomodular law pjomli 28866.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻) | ||
Theorem | pjhcl 28832 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ ℋ) | ||
Theorem | omlsilem 28833 | Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Sℋ & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐺 ⊆ 𝐻 & ⊢ (𝐻 ∩ (⊥‘𝐺)) = 0ℋ & ⊢ 𝐴 ∈ 𝐻 & ⊢ 𝐵 ∈ 𝐺 & ⊢ 𝐶 ∈ (⊥‘𝐺) ⇒ ⊢ (𝐴 = (𝐵 +ℎ 𝐶) → 𝐴 ∈ 𝐺) | ||
Theorem | omlsii 28834 | Subspace inference form of orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐴 ⊆ 𝐵 & ⊢ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | omlsi 28835 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵) | ||
Theorem | ococi 28836 | Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘(⊥‘𝐴)) = 𝐴 | ||
Theorem | ococ 28837 | Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (⊥‘(⊥‘𝐴)) = 𝐴) | ||
Theorem | dfch2 28838 | Alternate definition of the Hilbert lattice. (Contributed by NM, 8-Aug-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ Cℋ = {𝑥 ∈ 𝒫 ℋ ∣ (⊥‘(⊥‘𝑥)) = 𝑥} | ||
Theorem | ococin 28839* | The double complement is the smallest closed subspace containing a subset of Hilbert space. Remark 3.12(B) of [Beran] p. 107. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (⊥‘(⊥‘𝐴)) = ∩ {𝑥 ∈ Cℋ ∣ 𝐴 ⊆ 𝑥}) | ||
Theorem | hsupval2 28840* | Alternate definition of supremum of a subset of the Hilbert lattice. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice Cℋ, to allow more general theorems. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) = ∩ {𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥}) | ||
Theorem | chsupval2 28841* | The value of the supremum of a set of closed subspaces of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) = ∩ {𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥}) | ||
Theorem | sshjval2 28842* | Value of join in the set of closed subspaces of Hilbert space Cℋ. (Contributed by NM, 1-Nov-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) = ∩ {𝑥 ∈ Cℋ ∣ (𝐴 ∪ 𝐵) ⊆ 𝑥}) | ||
Theorem | chsupid 28843* | A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴}) = 𝐴) | ||
Theorem | chsupsn 28844 | Value of supremum of subset of Cℋ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝐴}) = 𝐴) | ||
Theorem | shlub 28845 | Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶)) | ||
Theorem | shlubi 28846 | Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
Theorem | pjhtheu2 28847* | Uniqueness of 𝑦 for the projection theorem. (Contributed by NM, 6-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ∃!𝑦 ∈ (⊥‘𝐻)∃𝑥 ∈ 𝐻 𝐴 = (𝑥 +ℎ 𝑦)) | ||
Theorem | pjcli 28848 | Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻) | ||
Theorem | pjhcli 28849 | Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ) | ||
Theorem | pjpjpre 28850 | Decomposition of a vector into projections. This formulation of axpjpj 28851 avoids pjhth 28824. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐻 ∈ Cℋ ) & ⊢ (𝜑 → 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) ⇒ ⊢ (𝜑 → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | axpjpj 28851 | Decomposition of a vector into projections. See comment in axpjcl 28831. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | pjclii 28852 | Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻 | ||
Theorem | pjhclii 28853 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ | ||
Theorem | pjpj0i 28854 | Decomposition of a vector into projections. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
Theorem | pjpji 28855 | Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
Theorem | pjpjhth 28856* | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦)) | ||
Theorem | pjpjhthi 28857* | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦) | ||
Theorem | pjop 28858 | Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))) | ||
Theorem | pjpo 28859 | Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | pjopi 28860 | Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
Theorem | pjpoi 28861 | Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
Theorem | pjoc1i 28862 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ 𝐻 ↔ ((projℎ‘(⊥‘𝐻))‘𝐴) = 0ℎ) | ||
Theorem | pjchi 28863 | Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ 𝐻 ↔ ((projℎ‘𝐻)‘𝐴) = 𝐴) | ||
Theorem | pjoccl 28864 | The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻)) | ||
Theorem | pjoc1 28865 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ ((projℎ‘(⊥‘𝐻))‘𝐴) = 0ℎ)) | ||
Theorem | pjomli 28866 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 28835. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵) | ||
Theorem | pjoml 28867 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 28835. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Sℋ ) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ)) → 𝐴 = 𝐵) | ||
Theorem | pjococi 28868 | Proof of orthocomplement theorem using projections. Compare ococ 28837. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (⊥‘(⊥‘𝐻)) = 𝐻 | ||
Theorem | pjoc2i 28869 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘𝐻) ↔ ((projℎ‘𝐻)‘𝐴) = 0ℎ) | ||
Theorem | pjoc2 28870 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ (⊥‘𝐻) ↔ ((projℎ‘𝐻)‘𝐴) = 0ℎ)) | ||
Theorem | sh0le 28871 | The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴) | ||
Theorem | ch0le 28872 | The zero subspace is the smallest member of Cℋ. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → 0ℋ ⊆ 𝐴) | ||
Theorem | shle0 28873 | No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
Theorem | chle0 28874 | No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
Theorem | chnlen0 28875 | A Hilbert lattice element that is not a subset of another is nonzero. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐵 ∈ Cℋ → (¬ 𝐴 ⊆ 𝐵 → ¬ 𝐴 = 0ℋ)) | ||
Theorem | ch0pss 28876 | The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (0ℋ ⊊ 𝐴 ↔ 𝐴 ≠ 0ℋ)) | ||
Theorem | orthin 28877 | The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ⊆ (⊥‘𝐵) → (𝐴 ∩ 𝐵) = 0ℋ)) | ||
Theorem | ssjo 28878 | The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ) | ||
Theorem | shne0i 28879* | A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
Theorem | shs0i 28880 | Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 0ℋ) = 𝐴 | ||
Theorem | shs00i 28881 | Two subspaces are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 = 0ℋ ∧ 𝐵 = 0ℋ) ↔ (𝐴 +ℋ 𝐵) = 0ℋ) | ||
Theorem | ch0lei 28882 | The closed subspace zero is the smallest member of Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 0ℋ ⊆ 𝐴 | ||
Theorem | chle0i 28883 | No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ) | ||
Theorem | chne0i 28884* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
Theorem | chocini 28885 | Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ (⊥‘𝐴)) = 0ℋ | ||
Theorem | chj0i 28886 | Join with lattice zero in Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 0ℋ) = 𝐴 | ||
Theorem | chm1i 28887 | Meet with lattice one in Cℋ. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ ℋ) = 𝐴 | ||
Theorem | chjcli 28888 | Closure of Cℋ join. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ | ||
Theorem | chsleji 28889 | Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | chseli 28890* | Membership in subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
Theorem | chincli 28891 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ | ||
Theorem | chsscon3i 28892 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴)) | ||
Theorem | chsscon1i 28893 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴) | ||
Theorem | chsscon2i 28894 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)) | ||
Theorem | chcon2i 28895 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = (⊥‘𝐵) ↔ 𝐵 = (⊥‘𝐴)) | ||
Theorem | chcon1i 28896 | Hilbert lattice contraposition law. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) = 𝐵 ↔ (⊥‘𝐵) = 𝐴) | ||
Theorem | chcon3i 28897 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = 𝐵 ↔ (⊥‘𝐵) = (⊥‘𝐴)) | ||
Theorem | chunssji 28898 | Union is smaller than Cℋ join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | chjcomi 28899 | Commutative law for join in Cℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
Theorem | chub1i 28900 | Cℋ join is an upper bound of two elements. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |