# Metamath Proof Explorer

## Theorem hhsst

Description: A member of SH is a subspace. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1
`|- U = <. <. +h , .h >. , normh >.`
hhsst.2
`|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
Assertion hhsst
`|- ( H e. SH -> W e. ( SubSp ` U ) )`

### Proof

Step Hyp Ref Expression
1 hhsst.1
` |-  U = <. <. +h , .h >. , normh >.`
2 hhsst.2
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
3 2 hhssnvt
` |-  ( H e. SH -> W e. NrmCVec )`
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 3 7 jctir
` |-  ( H e. SH -> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )`
9 1 hhnv
` |-  U e. NrmCVec`
10 1 hhva
` |-  +h = ( +v ` U )`
11 2 hhssva
` |-  ( +h |` ( H X. H ) ) = ( +v ` W )`
12 1 hhsm
` |-  .h = ( .sOLD ` U )`
13 2 hhsssm
` |-  ( .h |` ( CC X. H ) ) = ( .sOLD ` W )`
14 1 hhnm
` |-  normh = ( normCV ` U )`
15 2 hhssnm
` |-  ( normh |` H ) = ( normCV ` W )`
16 eqid
` |-  ( SubSp ` U ) = ( SubSp ` U )`
17 10 11 12 13 14 15 16 isssp
` |-  ( U e. NrmCVec -> ( W e. ( SubSp ` U ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) ) )`
18 9 17 ax-mp
` |-  ( W e. ( SubSp ` U ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )`
19 8 18 sylibr
` |-  ( H e. SH -> W e. ( SubSp ` U ) )`