This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjhcl

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

		Ref	Expression
	Assertion	pjhcl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in ℋ$

Step	Hyp	Ref	Expression
1		chss	$⊢ H \in C_{ℋ} \to H \subseteq ℋ$
2	1	adantr	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to H \subseteq ℋ$
3		axpjcl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in H$
4	2 3	sseldd	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in ℋ$