Theorem cldcss

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	cldcss	⊢ ( 𝑊 ∈ ℂHil → ( 𝑈 ∈ 𝐶 ↔ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cldcss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cldcss.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		cldcss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4		cldcss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
5		hlphl	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )
6	4 3	csslss	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝐶 ) → 𝑈 ∈ 𝐿 )
7	5 6	sylan	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐶 ) → 𝑈 ∈ 𝐿 )
8		hlcph	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
9	4 2	csscld	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝐶 ) → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
10	8 9	sylan	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐶 ) → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
11	7 10	jca	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐶 ) → ( 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )
12	5	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑊 ∈ PreHil )
13		eqid	⊢ ( proj ‘ 𝑊 ) = ( proj ‘ 𝑊 )
14	13 4	pjcss	⊢ ( 𝑊 ∈ PreHil → dom ( proj ‘ 𝑊 ) ⊆ 𝐶 )
15	12 14	syl	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → dom ( proj ‘ 𝑊 ) ⊆ 𝐶 )
16	2 3 13	pjth2	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ dom ( proj ‘ 𝑊 ) )
17	15 16	sseldd	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ 𝐶 )
18	17	3expb	⊢ ( ( 𝑊 ∈ ℂHil ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑈 ∈ 𝐶 )
19	11 18	impbida	⊢ ( 𝑊 ∈ ℂHil → ( 𝑈 ∈ 𝐶 ↔ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ) )