P. 314 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31301-31400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hsupcl 31301	Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to Cℋ even if the subsets do not. (Contributed by NM, 10-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ )
Theorem	chsupcl 31302	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 31303	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 31304	Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))
Theorem	hsupunss 31305	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 31306	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 31307	A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴))
Theorem	shsupunss 31308	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 31309	A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (span‘𝐴) = 𝐴)
Theorem	spanss 31310	Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵) → (span‘𝐴) ⊆ (span‘𝐵))
Theorem	spanssoc 31311	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 31312	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 31313	Value of join in Sℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjval 31314	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjvali 31315	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))
Theorem	sshjval3 31316	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 31317	Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcl 31318	Closure of join in Sℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	chjcl 31319	Closure of join in Cℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcom 31320	Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))
Theorem	shless 31321	Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1 31322	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 31323	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shincli 31324	Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ Sℋ
Theorem	shscomi 31325	Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)
Theorem	shsvai 31326	Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shsel1i 31327	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 31328	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 31329	Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shunssi 31330	Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 +ℋ 𝐵)
Theorem	shunssji 31331	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 31332	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 31333	Commutative law for join in Sℋ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)
Theorem	shsub1i 31334	Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 +ℋ 𝐵)
Theorem	shsub2i 31335	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐵 +ℋ 𝐴)
Theorem	shub1i 31336	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)
Theorem	shjcli 31337	Closure of Cℋ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
Theorem	shjshcli 31338	Sℋ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Sℋ
Theorem	shlessi 31339	Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1i 31340	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 31341	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shslej 31342	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 31343	Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∩ 𝐵) ∈ Sℋ )
Theorem	shub1 31344	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))
Theorem	shub2 31345	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 31346	Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐴) = 𝐴
Theorem	shslubi 31347	The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 +ℋ 𝐵) ⊆ 𝐶)
Theorem	shlesb1i 31348	Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 +ℋ 𝐵) = 𝐵)
Theorem	shsval2i 31349*	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = ∩ {𝑥 ∈ Sℋ ∣ (𝐴 ∪ 𝐵) ⊆ 𝑥}
Theorem	shsval3i 31350	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (span‘(𝐴 ∪ 𝐵))
Theorem	shmodsi 31351	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 31352	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 31353*	Lemma for pjhth 31355. (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 31354*	Lemma for pjhth 31355. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ (𝜑 → 𝐴 ∈ ℋ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))
Theorem	pjhth 31355	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 31356*	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 31378 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 31357*	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 31358*	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 31359*	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 31360*	Equality with a projection. This version of pjeq 31361 does not assume the Axiom of Choice via pjhth 31355. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥))))
Theorem	pjeq 31361*	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 31362	Closure of a projection in its subspace. If we consider this together with axpjpj 31382 to be axioms, the need for the ax-hcompl 31164 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 31397.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcl 31363	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 31364	Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐺 ⊆ 𝐻    &   ⊢ (𝐻 ∩ (⊥‘𝐺)) = 0ℋ    &   ⊢ 𝐴 ∈ 𝐻    &   ⊢ 𝐵 ∈ 𝐺    &   ⊢ 𝐶 ∈ (⊥‘𝐺)    ⇒   ⊢ (𝐴 = (𝐵 +ℎ 𝐶) → 𝐴 ∈ 𝐺)
Theorem	omlsii 31365	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 31366	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 31367	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 31368	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 31369	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 31370*	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 31371*	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 31372*	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 31373*	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 31374*	A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴}) = 𝐴)
Theorem	chsupsn 31375	Value of supremum of subset of Cℋ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝐴}) = 𝐴)
Theorem	shlub 31376	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 31377	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 31378*	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 31379	Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcli 31380	Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
Theorem	pjpjpre 31381	Decomposition of a vector into projections. This formulation of axpjpj 31382 avoids pjhth 31355. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐻 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻)))    ⇒   ⊢ (𝜑 → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	axpjpj 31382	Decomposition of a vector into projections. See comment in axpjcl 31362. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjclii 31383	Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻
Theorem	pjhclii 31384	Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ
Theorem	pjpj0i 31385	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 31386	Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
Theorem	pjpjhth 31387*	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 31388*	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 31389	Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjpo 31390	Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjopi 31391	Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjpoi 31392	Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
Theorem	pjoc1i 31393	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 31394	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 31395	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 31396	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 31397	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 31366. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵)
Theorem	pjoml 31398	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 31366. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Sℋ ) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ)) → 𝐴 = 𝐵)
Theorem	pjococi 31399	Proof of orthocomplement theorem using projections. Compare ococ 31368. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (⊥‘(⊥‘𝐻)) = 𝐻
Theorem	pjoc2i 31400	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ℎ)