Metamath Proof Explorer

Theorem sspid

Description: A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis sspid.h 
|- H = ( SubSp ` U )
Assertion sspid 
|- ( U e. NrmCVec -> U e. H )

Proof

Step Hyp Ref Expression
1 sspid.h 
 |-  H = ( SubSp ` U )
2 ssid 
 |-  ( +v ` U ) C_ ( +v ` U )
3 ssid 
 |-  ( .sOLD ` U ) C_ ( .sOLD ` U )
4 ssid 
 |-  ( normCV ` U ) C_ ( normCV ` U )
5 2 3 4 3pm3.2i 
 |-  ( ( +v ` U ) C_ ( +v ` U ) /\ ( .sOLD ` U ) C_ ( .sOLD ` U ) /\ ( normCV ` U ) C_ ( normCV ` U ) )
6 5 jctr 
 |-  ( U e. NrmCVec -> ( U e. NrmCVec /\ ( ( +v ` U ) C_ ( +v ` U ) /\ ( .sOLD ` U ) C_ ( .sOLD ` U ) /\ ( normCV ` U ) C_ ( normCV ` U ) ) ) )
7 eqid 
 |-  ( +v ` U ) = ( +v ` U )
8 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
9 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
10 7 7 8 8 9 9 1 isssp 
 |-  ( U e. NrmCVec -> ( U e. H <-> ( U e. NrmCVec /\ ( ( +v ` U ) C_ ( +v ` U ) /\ ( .sOLD ` U ) C_ ( .sOLD ` U ) /\ ( normCV ` U ) C_ ( normCV ` U ) ) ) ) )
11 6 10 mpbird 
 |-  ( U e. NrmCVec -> U e. H )