Metamath Proof Explorer


Theorem isch

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

Proof

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