Theorem 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 {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge \underset{v}{⇝}\left[H^{\mathbb{N}}\right]\subseteq H\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢h=H\to h^{\mathbb{N}}=H^{\mathbb{N}}$$
2	1	imaeq2d	$$⊢h=H\to \underset{v}{⇝}\left[h^{\mathbb{N}}\right]=\underset{v}{⇝}\left[H^{\mathbb{N}}\right]$$
3		id	$$⊢h=H\to h=H$$
4	2 3	sseq12d	$$⊢h=H\to \left(\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h\leftrightarrow \underset{v}{⇝}\left[H^{\mathbb{N}}\right]\subseteq H\right)$$
5		df-ch	$$⊢{\mathbf{C}}_{\mathscr{H}}=\left\{h\in {\mathbf{S}}_{\mathscr{H}}|\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h\right\}$$
6	4 5	elrab2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge \underset{v}{⇝}\left[H^{\mathbb{N}}\right]\subseteq H\right)$$