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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cldcss.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	cldcss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
	cldcss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion	cldcss2	⊢ ( 𝑊 ∈ ℂHil → 𝐶 = ( 𝐿 ∩ ( Clsd ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cldcss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cldcss.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		cldcss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4		cldcss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
5	1 2 3 4	cldcss	⊢ ( 𝑊 ∈ ℂHil → ( 𝑥 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐿 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) )
6		elin	⊢ ( 𝑥 ∈ ( 𝐿 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ( 𝑥 ∈ 𝐿 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
7	5 6	bitr4di	⊢ ( 𝑊 ∈ ℂHil → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ( 𝐿 ∩ ( Clsd ‘ 𝐽 ) ) ) )
8	7	eqrdv	⊢ ( 𝑊 ∈ ℂHil → 𝐶 = ( 𝐿 ∩ ( Clsd ‘ 𝐽 ) ) )