# Metamath Proof Explorer

## Theorem hhsssh2

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhsssh2.1
`|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
Assertion hhsssh2
`|- ( H e. SH <-> ( W e. NrmCVec /\ H C_ ~H ) )`

### Proof

Step Hyp Ref Expression
1 hhsssh2.1
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
2 eqid
` |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.`
3 2 1 hhsssh
` |-  ( H e. SH <-> ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) /\ H C_ ~H ) )`
4 resss
` |-  ( +h |` ( H X. H ) ) C_ +h`
5 resss
` |-  ( .h |` ( CC X. H ) ) C_ .h`
6 resss
` |-  ( normh |` H ) C_ normh`
7 4 5 6 3pm3.2i
` |-  ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh )`
8 2 hhnv
` |-  <. <. +h , .h >. , normh >. e. NrmCVec`
9 2 hhva
` |-  +h = ( +v ` <. <. +h , .h >. , normh >. )`
10 1 hhssva
` |-  ( +h |` ( H X. H ) ) = ( +v ` W )`
11 2 hhsm
` |-  .h = ( .sOLD ` <. <. +h , .h >. , normh >. )`
12 1 hhsssm
` |-  ( .h |` ( CC X. H ) ) = ( .sOLD ` W )`
13 2 hhnm
` |-  normh = ( normCV ` <. <. +h , .h >. , normh >. )`
14 1 hhssnm
` |-  ( normh |` H ) = ( normCV ` W )`
15 eqid
` |-  ( SubSp ` <. <. +h , .h >. , normh >. ) = ( SubSp ` <. <. +h , .h >. , normh >. )`
16 9 10 11 12 13 14 15 isssp
` |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) ) )`
17 8 16 ax-mp
` |-  ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )`
18 7 17 mpbiran2
` |-  ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> W e. NrmCVec )`
19 18 anbi1i
` |-  ( ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) /\ H C_ ~H ) <-> ( W e. NrmCVec /\ H C_ ~H ) )`
20 3 19 bitri
` |-  ( H e. SH <-> ( W e. NrmCVec /\ H C_ ~H ) )`