P. 317 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31601-31700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chsupcl 31601	Closure of supremum of subset of Cℋ. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that Cℋ is a complete lattice. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 10-Nov-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ )
Theorem	hsupss 31602	Subset relation for supremum of Hilbert space subsets. (Contributed by NM, 24-Nov-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))
Theorem	chsupss 31603	Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))
Theorem	hsupunss 31604	The union of a set of Hilbert space subsets is smaller than its supremum. (Contributed by NM, 24-Nov-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → ∪ 𝐴 ⊆ ( ∨ℋ ‘𝐴))
Theorem	chsupunss 31605	The union of a set of closed subspaces is smaller than its supremum. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ → ∪ 𝐴 ⊆ ( ∨ℋ ‘𝐴))
Theorem	spanss2 31606	A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴))
Theorem	shsupunss 31607	The union of a set of subspaces is smaller than its supremum. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ (span‘∪ 𝐴))
Theorem	spanid 31608	A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (span‘𝐴) = 𝐴)
Theorem	spanss 31609	Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵) → (span‘𝐴) ⊆ (span‘𝐵))
Theorem	spanssoc 31610	The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement). (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) ⊆ (⊥‘(⊥‘𝐴)))
Theorem	sshjval 31611	Value of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	shjval 31612	Value of join in Sℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjval 31613	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjvali 31614	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))
Theorem	sshjval3 31615	Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice Cℋ. (Contributed by NM, 2-Mar-2004.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) = ( ∨ℋ ‘{𝐴, 𝐵}))
Theorem	sshjcl 31616	Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcl 31617	Closure of join in Sℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	chjcl 31618	Closure of join in Cℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcom 31619	Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))
Theorem	shless 31620	Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1 31621	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶))
Theorem	shlej2 31622	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shincli 31623	Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ Sℋ
Theorem	shscomi 31624	Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)
Theorem	shsvai 31625	Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shsel1i 31626	A subspace sum contains a member of one of its subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ (𝐴 +ℋ 𝐵))
Theorem	shsel2i 31627	A subspace sum contains a member of one of its subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ (𝐴 +ℋ 𝐵))
Theorem	shsvsi 31628	Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shunssi 31629	Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 +ℋ 𝐵)
Theorem	shunssji 31630	Union is smaller than Hilbert lattice join. (Contributed by NM, 11-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵)
Theorem	shsleji 31631	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 31632	Commutative law for join in Sℋ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)
Theorem	shsub1i 31633	Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 +ℋ 𝐵)
Theorem	shsub2i 31634	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐵 +ℋ 𝐴)
Theorem	shub1i 31635	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)
Theorem	shjcli 31636	Closure of Cℋ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
Theorem	shjshcli 31637	Sℋ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Sℋ
Theorem	shlessi 31638	Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1i 31639	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 31640	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shslej 31641	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 31642	Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∩ 𝐵) ∈ Sℋ )
Theorem	shub1 31643	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))
Theorem	shub2 31644	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 31645	Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐴) = 𝐴
Theorem	shslubi 31646	The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 +ℋ 𝐵) ⊆ 𝐶)
Theorem	shlesb1i 31647	Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 +ℋ 𝐵) = 𝐵)
Theorem	shsval2i 31648*	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = ∩ {𝑥 ∈ Sℋ ∣ (𝐴 ∪ 𝐵) ⊆ 𝑥}
Theorem	shsval3i 31649	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (span‘(𝐴 ∪ 𝐵))
Theorem	shmodsi 31650	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 31651	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ℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ 𝐶) → ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) ⊆ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)))
20.4.5  Projection theorem
Theorem	pjhthlem1 31652*	Lemma for pjhth 31654. (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 31653*	Lemma for pjhth 31654. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ (𝜑 → 𝐴 ∈ ℋ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))
Theorem	pjhth 31654	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 31655*	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 31677 for the uniqueness of 𝑦. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ∃!𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))
20.4.6  Projectors
Definition	df-pjh 31656*	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 31657*	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 31658*	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 31659*	Equality with a projection. This version of pjeq 31660 does not assume the Axiom of Choice via pjhth 31654. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥))))
Theorem	pjeq 31660*	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 31661	Closure of a projection in its subspace. If we consider this together with axpjpj 31681 to be axioms, the need for the ax-hcompl 31463 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 31696.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcl 31662	Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
20.5  Properties of Hilbert subspaces
20.5.1  Orthomodular law
Theorem	omlsilem 31663	Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐺 ⊆ 𝐻    &   ⊢ (𝐻 ∩ (⊥‘𝐺)) = 0ℋ    &   ⊢ 𝐴 ∈ 𝐻    &   ⊢ 𝐵 ∈ 𝐺    &   ⊢ 𝐶 ∈ (⊥‘𝐺)    ⇒   ⊢ (𝐴 = (𝐵 +ℎ 𝐶) → 𝐴 ∈ 𝐺)
Theorem	omlsii 31664	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 31665	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 31666	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 31667	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 31668	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 31669*	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 31670*	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 31671*	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 31672*	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 31673*	A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴}) = 𝐴)
Theorem	chsupsn 31674	Value of supremum of subset of Cℋ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝐴}) = 𝐴)
Theorem	shlub 31675	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 31676	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ℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶)
20.5.2  Projectors (cont.)
Theorem	pjhtheu2 31677*	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 31678	Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcli 31679	Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
Theorem	pjpjpre 31680	Decomposition of a vector into projections. This formulation of axpjpj 31681 avoids pjhth 31654. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐻 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻)))    ⇒   ⊢ (𝜑 → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	axpjpj 31681	Decomposition of a vector into projections. See comment in axpjcl 31661. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjclii 31682	Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻
Theorem	pjhclii 31683	Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ
Theorem	pjpj0i 31684	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 31685	Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
Theorem	pjpjhth 31686*	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 31687*	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 31688	Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjpo 31689	Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjopi 31690	Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjpoi 31691	Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
Theorem	pjoc1i 31692	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 31693	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 31694	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 31695	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 31696	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 31665. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵)
Theorem	pjoml 31697	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 31665. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Sℋ ) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ)) → 𝐴 = 𝐵)
Theorem	pjococi 31698	Proof of orthocomplement theorem using projections. Compare ococ 31667. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (⊥‘(⊥‘𝐻)) = 𝐻
Theorem	pjoc2i 31699	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 31700	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ℎ))