Metamath Proof Explorer

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 ⊢ V = Base W
cldcss.j ⊢ J = TopOpen ⁡ W
cldcss.l ⊢ L = LSubSp ⁡ W
cldcss.c ⊢ C = ClSubSp ⁡ W
Assertion cldcss ⊢ W ∈ ℂHil → U ∈ C ↔ U ∈ L ∧ U ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 cldcss.v ⊢ V = Base W
2 cldcss.j ⊢ J = TopOpen ⁡ W
3 cldcss.l ⊢ L = LSubSp ⁡ W
4 cldcss.c ⊢ C = ClSubSp ⁡ W
5 hlphl ⊢ W ∈ ℂHil → W ∈ PreHil
6 4 3 csslss ⊢ W ∈ PreHil ∧ U ∈ C → U ∈ L
7 5 6 sylan ⊢ W ∈ ℂHil ∧ U ∈ C → U ∈ L
8 hlcph ⊢ W ∈ ℂHil → W ∈ CPreHil
9 4 2 csscld ⊢ W ∈ CPreHil ∧ U ∈ C → U ∈ Clsd ⁡ J
10 8 9 sylan ⊢ W ∈ ℂHil ∧ U ∈ C → U ∈ Clsd ⁡ J
11 7 10 jca ⊢ W ∈ ℂHil ∧ U ∈ C → U ∈ L ∧ U ∈ Clsd ⁡ J
12 5 3ad2ant1 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → W ∈ PreHil
13 eqid ⊢ proj ⁡ W = proj ⁡ W
14 13 4 pjcss ⊢ W ∈ PreHil → dom ⁡ proj ⁡ W ⊆ C
15 12 14 syl ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → dom ⁡ proj ⁡ W ⊆ C
16 2 3 13 pjth2 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ∈ dom ⁡ proj ⁡ W
17 15 16 sseldd ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ∈ C
18 17 3expb ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ∈ C
19 11 18 impbida ⊢ W ∈ ℂHil → U ∈ C ↔ U ∈ L ∧ U ∈ Clsd ⁡ J