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 | cldcss2 | |- ( W e. CHil -> C = ( L i^i ( Clsd ` J ) ) ) |
| 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 | 1 2 3 4 | cldcss | |- ( W e. CHil -> ( x e. C <-> ( x e. L /\ x e. ( Clsd ` J ) ) ) ) |
| 6 | elin | |- ( x e. ( L i^i ( Clsd ` J ) ) <-> ( x e. L /\ x e. ( Clsd ` J ) ) ) |
|
| 7 | 5 6 | bitr4di | |- ( W e. CHil -> ( x e. C <-> x e. ( L i^i ( Clsd ` J ) ) ) ) |
| 8 | 7 | eqrdv | |- ( W e. CHil -> C = ( L i^i ( Clsd ` J ) ) ) |