Home | Metamath
Proof Explorer Theorem List (p. 292 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pjhfval 29101* | 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 29102* | 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 29103* | Equality with a projection. This version of pjeq 29104 does not assume the Axiom of Choice via pjhth 29098. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)))) | ||
Theorem | pjeq 29104* | 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 29105 | Closure of a projection in its subspace. If we consider this together with axpjpj 29125 to be axioms, the need for the ax-hcompl 28907 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 29140.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻) | ||
Theorem | pjhcl 29106 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ ℋ) | ||
Theorem | omlsilem 29107 | Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Sℋ & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐺 ⊆ 𝐻 & ⊢ (𝐻 ∩ (⊥‘𝐺)) = 0ℋ & ⊢ 𝐴 ∈ 𝐻 & ⊢ 𝐵 ∈ 𝐺 & ⊢ 𝐶 ∈ (⊥‘𝐺) ⇒ ⊢ (𝐴 = (𝐵 +ℎ 𝐶) → 𝐴 ∈ 𝐺) | ||
Theorem | omlsii 29108 | 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 29109 | 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 29110 | 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 29111 | 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 29112 | 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 29113* | 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 29114* | 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 29115* | 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 29116* | 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 29117* | A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴}) = 𝐴) | ||
Theorem | chsupsn 29118 | Value of supremum of subset of Cℋ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝐴}) = 𝐴) | ||
Theorem | shlub 29119 | 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 29120 | 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 29121* | 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 29122 | Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻) | ||
Theorem | pjhcli 29123 | Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ) | ||
Theorem | pjpjpre 29124 | Decomposition of a vector into projections. This formulation of axpjpj 29125 avoids pjhth 29098. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐻 ∈ Cℋ ) & ⊢ (𝜑 → 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) ⇒ ⊢ (𝜑 → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | axpjpj 29125 | Decomposition of a vector into projections. See comment in axpjcl 29105. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | pjclii 29126 | Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻 | ||
Theorem | pjhclii 29127 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ | ||
Theorem | pjpj0i 29128 | 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 29129 | Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
Theorem | pjpjhth 29130* | 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 29131* | 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 29132 | Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))) | ||
Theorem | pjpo 29133 | Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
Theorem | pjopi 29134 | Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
Theorem | pjpoi 29135 | Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
Theorem | pjoc1i 29136 | 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 29137 | 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 29138 | 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 29139 | 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 29140 | 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 29109. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵) | ||
Theorem | pjoml 29141 | 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 29109. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Sℋ ) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ)) → 𝐴 = 𝐵) | ||
Theorem | pjococi 29142 | Proof of orthocomplement theorem using projections. Compare ococ 29111. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (⊥‘(⊥‘𝐻)) = 𝐻 | ||
Theorem | pjoc2i 29143 | 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 29144 | 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 29145 | The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴) | ||
Theorem | ch0le 29146 | The zero subspace is the smallest member of Cℋ. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → 0ℋ ⊆ 𝐴) | ||
Theorem | shle0 29147 | No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
Theorem | chle0 29148 | No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
Theorem | chnlen0 29149 | 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 29150 | 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 29151 | The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ⊆ (⊥‘𝐵) → (𝐴 ∩ 𝐵) = 0ℋ)) | ||
Theorem | ssjo 29152 | 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 29153* | A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
Theorem | shs0i 29154 | Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 0ℋ) = 𝐴 | ||
Theorem | shs00i 29155 | 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 29156 | The closed subspace zero is the smallest member of Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 0ℋ ⊆ 𝐴 | ||
Theorem | chle0i 29157 | No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ) | ||
Theorem | chne0i 29158* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
Theorem | chocini 29159 | 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 29160 | Join with lattice zero in Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 0ℋ) = 𝐴 | ||
Theorem | chm1i 29161 | Meet with lattice one in Cℋ. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ ℋ) = 𝐴 | ||
Theorem | chjcli 29162 | Closure of Cℋ join. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ | ||
Theorem | chsleji 29163 | 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 29164* | Membership in subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
Theorem | chincli 29165 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ | ||
Theorem | chsscon3i 29166 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴)) | ||
Theorem | chsscon1i 29167 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴) | ||
Theorem | chsscon2i 29168 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)) | ||
Theorem | chcon2i 29169 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = (⊥‘𝐵) ↔ 𝐵 = (⊥‘𝐴)) | ||
Theorem | chcon1i 29170 | Hilbert lattice contraposition law. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) = 𝐵 ↔ (⊥‘𝐵) = 𝐴) | ||
Theorem | chcon3i 29171 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = 𝐵 ↔ (⊥‘𝐵) = (⊥‘𝐴)) | ||
Theorem | chunssji 29172 | Union is smaller than Cℋ join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | chjcomi 29173 | Commutative law for join in Cℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
Theorem | chub1i 29174 | Cℋ join is an upper bound of two elements. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | chub2i 29175 | Cℋ join is an upper bound of two elements. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐵 ∨ℋ 𝐴) | ||
Theorem | chlubi 29176 | Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
Theorem | chlubii 29177 | Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 29176). (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
Theorem | chlej1i 29178 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | chlej2i 29179 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
Theorem | chlej12i 29180 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐷)) | ||
Theorem | chlejb1i 29181 | Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵) | ||
Theorem | chdmm1i 29182 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)) | ||
Theorem | chdmm2i 29183 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵)) | ||
Theorem | chdmm3i 29184 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵) | ||
Theorem | chdmm4i 29185 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵) | ||
Theorem | chdmj1i 29186 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵)) | ||
Theorem | chdmj2i 29187 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵)) | ||
Theorem | chdmj3i 29188 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵) | ||
Theorem | chdmj4i 29189 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵) | ||
Theorem | chnlei 29190 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | chjassi 29191 | Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | chj00i 29192 | Two Hilbert lattice elements are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 = 0ℋ ∧ 𝐵 = 0ℋ) ↔ (𝐴 ∨ℋ 𝐵) = 0ℋ) | ||
Theorem | chjoi 29193 | The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ | ||
Theorem | chj1i 29194 | Join with Hilbert lattice unit. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ℋ) = ℋ | ||
Theorem | chm0i 29195 | Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 0ℋ) = 0ℋ | ||
Theorem | chm0 29196 | Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ 0ℋ) = 0ℋ) | ||
Theorem | shjshsi 29197 | Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 +ℋ 𝐵))) | ||
Theorem | shjshseli 29198 | A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 +ℋ 𝐵) ∈ Cℋ ↔ (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | chne0 29199* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ)) | ||
Theorem | chocin 29200 | Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |