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 )