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

Metamath Proof Explorer

Theorem pjhcli

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

		Ref	Expression
	Hypothesis	pjcl.1	$⊢ H \in C_{ℋ}$
	Assertion	pjhcli	$⊢ A \in ℋ \to {proj}_{ℎ} (H) (A) \in ℋ$

Step	Hyp	Ref	Expression
1		pjcl.1	$⊢ H \in C_{ℋ}$
2		pjhcl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in ℋ$
3	1 2	mpan	$⊢ A \in ℋ \to {proj}_{ℎ} (H) (A) \in ℋ$