# Metamath Proof Explorer

## Theorem hhssnvt

Description: Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hhssnvt.1
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
2 xpeq1
` |-  ( H = if ( H e. SH , H , 0H ) -> ( H X. H ) = ( if ( H e. SH , H , 0H ) X. H ) )`
3 xpeq2
` |-  ( H = if ( H e. SH , H , 0H ) -> ( if ( H e. SH , H , 0H ) X. H ) = ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) )`
4 2 3 eqtrd
` |-  ( H = if ( H e. SH , H , 0H ) -> ( H X. H ) = ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) )`
5 4 reseq2d
` |-  ( H = if ( H e. SH , H , 0H ) -> ( +h |` ( H X. H ) ) = ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) )`
6 xpeq2
` |-  ( H = if ( H e. SH , H , 0H ) -> ( CC X. H ) = ( CC X. if ( H e. SH , H , 0H ) ) )`
7 6 reseq2d
` |-  ( H = if ( H e. SH , H , 0H ) -> ( .h |` ( CC X. H ) ) = ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) )`
8 5 7 opeq12d
` |-  ( H = if ( H e. SH , H , 0H ) -> <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. = <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. )`
9 reseq2
` |-  ( H = if ( H e. SH , H , 0H ) -> ( normh |` H ) = ( normh |` if ( H e. SH , H , 0H ) ) )`
10 8 9 opeq12d
` |-  ( H = if ( H e. SH , H , 0H ) -> <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. = <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >. )`
11 1 10 syl5eq
` |-  ( H = if ( H e. SH , H , 0H ) -> W = <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >. )`
12 11 eleq1d
` |-  ( H = if ( H e. SH , H , 0H ) -> ( W e. NrmCVec <-> <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >. e. NrmCVec ) )`
13 eqid
` |-  <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >. = <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >.`
14 h0elsh
` |-  0H e. SH`
15 14 elimel
` |-  if ( H e. SH , H , 0H ) e. SH`
16 13 15 hhssnv
` |-  <. <. ( +h |` ( if ( H e. SH , H , 0H ) X. if ( H e. SH , H , 0H ) ) ) , ( .h |` ( CC X. if ( H e. SH , H , 0H ) ) ) >. , ( normh |` if ( H e. SH , H , 0H ) ) >. e. NrmCVec`
17 12 16 dedth
` |-  ( H e. SH -> W e. NrmCVec )`