Theorem pjhcl

Description: Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhcl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		chss	⊢ ( 𝐻 ∈ Cℋ → 𝐻 ⊆ ℋ )
2	1	adantr	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐻 ⊆ ℋ )
3		axpjcl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )
4	2 3	sseldd	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )