Theorem cldcss2

Description: Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015)

	Ref	Expression
Hypotheses	cldcss.v	$$⊢V={\mathrm{Base}}_W$$
	cldcss.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	cldcss.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
	cldcss.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
Assertion	cldcss2	$$⊢W\in \mathrm{ℂHil}\to C=L\cap \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		cldcss.v	$$⊢V={\mathrm{Base}}_W$$
2		cldcss.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		cldcss.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
4		cldcss.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
5	1 2 3 4	cldcss	$$⊢W\in \mathrm{ℂHil}\to \left(x\in C\leftrightarrow \left(x\in L\wedge x\in \mathrm{Clsd}\left(J\right)\right)\right)$$
6		elin	$$⊢x\in \left(L\cap \mathrm{Clsd}\left(J\right)\right)\leftrightarrow \left(x\in L\wedge x\in \mathrm{Clsd}\left(J\right)\right)$$
7	5 6	bitr4di	$$⊢W\in \mathrm{ℂHil}\to \left(x\in C\leftrightarrow x\in \left(L\cap \mathrm{Clsd}\left(J\right)\right)\right)$$
8	7	eqrdv	$$⊢W\in \mathrm{ℂHil}\to C=L\cap \mathrm{Clsd}\left(J\right)$$