P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

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ℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ 𝐶) → ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) ⊆ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)))
19.4.5  Projection theorem
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ℋ ∧ 𝐴 ∈ ℋ) → ∃!𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))
19.4.6  Projectors
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ℎ‘𝐻)‘𝐴) ∈ ℋ)
19.5  Properties of Hilbert subspaces
19.5.1  Orthomodular law
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ℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶)
19.5.2  Projectors (cont.)
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ℎ))
19.5.3  Hilbert lattice operations
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ℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)