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 ) ) |