Metamath Proof Explorer

Theorem sspnv

Description: A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypothesis sspnv.h 
|- H = ( SubSp ` U )
Assertion sspnv 
|- ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )

Proof

Step Hyp Ref Expression
1 sspnv.h 
 |-  H = ( SubSp ` U )
2 eqid 
 |-  ( +v ` U ) = ( +v ` U )
3 eqid 
 |-  ( +v ` W ) = ( +v ` W )
4 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
5 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
6 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
7 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
8 2 3 4 5 6 7 1 isssp 
 |-  ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( ( +v ` W ) C_ ( +v ` U ) /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ ( normCV ` W ) C_ ( normCV ` U ) ) ) ) )
9 8 simprbda 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )