isch

Description: Closed subspace H of a Hilbert space. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	isch	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \underset{v}{⇝} [H^{ℕ}] \subseteq H)$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ h = H \to h^{ℕ} = H^{ℕ}$
2	1	imaeq2d	$⊢ h = H \to \underset{v}{⇝} [h^{ℕ}] = \underset{v}{⇝} [H^{ℕ}]$
3		id	$⊢ h = H \to h = H$
4	2 3	sseq12d	$⊢ h = H \to (\underset{v}{⇝} [h^{ℕ}] \subseteq h \leftrightarrow \underset{v}{⇝} [H^{ℕ}] \subseteq H)$
5		df-ch	$⊢ C_{ℋ} = \{h \in S_{ℋ} \| \underset{v}{⇝} [h^{ℕ}] \subseteq h\}$
6	4 5	elrab2	$⊢ H \in C_{ℋ} \leftrightarrow (H \in S_{ℋ} \land \underset{v}{⇝} [H^{ℕ}] \subseteq H)$

Metamath Proof Explorer

Theorem isch

Proof