P. 298 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29701-29800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	shintcl 29701	The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Sℋ )
Theorem	chintcli 29702	The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅)    ⇒   ⊢ ∩ 𝐴 ∈ Cℋ
Theorem	chintcl 29703	The intersection (infimum) of a nonempty subset of Cℋ belongs to Cℋ. Part of Theorem 3.13 of [Beran] p. 108. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Cℋ )
Theorem	spanval 29704*	Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in [Schechter] p. 276. (Contributed by NM, 2-Jun-2004.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) = ∩ {𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥})
Theorem	hsupval 29705	Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 29780. (Contributed by NM, 9-Dec-2003.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴)))
Theorem	chsupval 29706	The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 29781. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴)))
Theorem	spancl 29707	The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) ∈ Sℋ )
Theorem	elspancl 29708	A member of a span is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ∈ (span‘𝐴)) → 𝐵 ∈ ℋ)
Theorem	shsupcl 29709	Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 ℋ → (span‘∪ 𝐴) ∈ Sℋ )
Theorem	hsupcl 29710	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 29711	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 29712	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 29713	Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵)))
Theorem	hsupunss 29714	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 29715	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 29716	A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴))
Theorem	shsupunss 29717	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 29718	A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (span‘𝐴) = 𝐴)
Theorem	spanss 29719	Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵) → (span‘𝐴) ⊆ (span‘𝐵))
Theorem	spanssoc 29720	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 29721	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 29722	Value of join in Sℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjval 29723	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))))
Theorem	chjvali 29724	Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))
Theorem	sshjval3 29725	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 29726	Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcl 29727	Closure of join in Sℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	chjcl 29728	Closure of join in Cℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
Theorem	shjcom 29729	Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))
Theorem	shless 29730	Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1 29731	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 29732	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shincli 29733	Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ Sℋ
Theorem	shscomi 29734	Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)
Theorem	shsvai 29735	Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shsel1i 29736	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 29737	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 29738	Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))
Theorem	shunssi 29739	Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 +ℋ 𝐵)
Theorem	shunssji 29740	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 29741	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 29742	Commutative law for join in Sℋ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)
Theorem	shsub1i 29743	Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 +ℋ 𝐵)
Theorem	shsub2i 29744	Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐵 +ℋ 𝐴)
Theorem	shub1i 29745	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)
Theorem	shjcli 29746	Closure of Cℋ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
Theorem	shjshcli 29747	Sℋ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) ∈ Sℋ
Theorem	shlessi 29748	Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶))
Theorem	shlej1i 29749	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 29750	Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵))
Theorem	shslej 29751	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 29752	Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∩ 𝐵) ∈ Sℋ )
Theorem	shub1 29753	Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))
Theorem	shub2 29754	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 29755	Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐴) = 𝐴
Theorem	shslubi 29756	The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    ⇒   ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 +ℋ 𝐵) ⊆ 𝐶)
Theorem	shlesb1i 29757	Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 +ℋ 𝐵) = 𝐵)
Theorem	shsval2i 29758*	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = ∩ {𝑥 ∈ Sℋ ∣ (𝐴 ∪ 𝐵) ⊆ 𝑥}
Theorem	shsval3i 29759	An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (𝐴 +ℋ 𝐵) = (span‘(𝐴 ∪ 𝐵))
Theorem	shmodsi 29760	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 29761	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 29762*	Lemma for pjhth 29764. (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 29763*	Lemma for pjhth 29764. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ (𝜑 → 𝐴 ∈ ℋ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦))
Theorem	pjhth 29764	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 29765*	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 29787 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 29766*	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 29767*	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 29768*	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 29769*	Equality with a projection. This version of pjeq 29770 does not assume the Axiom of Choice via pjhth 29764. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥))))
Theorem	pjeq 29770*	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 29771	Closure of a projection in its subspace. If we consider this together with axpjpj 29791 to be axioms, the need for the ax-hcompl 29573 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 29806.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcl 29772	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 29773	Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝐻 ∈ Sℋ    &   ⊢ 𝐺 ⊆ 𝐻    &   ⊢ (𝐻 ∩ (⊥‘𝐺)) = 0ℋ    &   ⊢ 𝐴 ∈ 𝐻    &   ⊢ 𝐵 ∈ 𝐺    &   ⊢ 𝐶 ∈ (⊥‘𝐺)    ⇒   ⊢ (𝐴 = (𝐵 +ℎ 𝐶) → 𝐴 ∈ 𝐺)
Theorem	omlsii 29774	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 29775	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 29776	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 29777	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 29778	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 29779*	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 29780*	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 29781*	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 29782*	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 29783*	A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴}) = 𝐴)
Theorem	chsupsn 29784	Value of supremum of subset of Cℋ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ( ∨ℋ ‘{𝐴}) = 𝐴)
Theorem	shlub 29785	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 29786	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 29787*	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 29788	Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ 𝐻)
Theorem	pjhcli 29789	Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
Theorem	pjpjpre 29790	Decomposition of a vector into projections. This formulation of axpjpj 29791 avoids pjhth 29764. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐻 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻)))    ⇒   ⊢ (𝜑 → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	axpjpj 29791	Decomposition of a vector into projections. See comment in axpjcl 29771. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjclii 29792	Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ 𝐻
Theorem	pjhclii 29793	Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘𝐴) ∈ ℋ
Theorem	pjpj0i 29794	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 29795	Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ 𝐴 = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))
Theorem	pjpjhth 29796*	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 29797*	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 29798	Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjpo 29799	Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)))
Theorem	pjopi 29800	Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))