Description: Closed subspace H of a Hilbert space. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isch | |- ( H e. CH <-> ( H e. SH /\ ( ~~>v " ( H ^m NN ) ) C_ H ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq1 | |- ( h = H -> ( h ^m NN ) = ( H ^m NN ) ) |
|
| 2 | 1 | imaeq2d | |- ( h = H -> ( ~~>v " ( h ^m NN ) ) = ( ~~>v " ( H ^m NN ) ) ) |
| 3 | id | |- ( h = H -> h = H ) |
|
| 4 | 2 3 | sseq12d | |- ( h = H -> ( ( ~~>v " ( h ^m NN ) ) C_ h <-> ( ~~>v " ( H ^m NN ) ) C_ H ) ) |
| 5 | df-ch | |- CH = { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h } |
|
| 6 | 4 5 | elrab2 | |- ( H e. CH <-> ( H e. SH /\ ( ~~>v " ( H ^m NN ) ) C_ H ) ) |