Metamath Proof Explorer

Theorem sspba

Description: The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspba.x 
|- X = ( BaseSet ` U )
sspba.y 
|- Y = ( BaseSet ` W )
sspba.h 
|- H = ( SubSp ` U )
Assertion sspba 
|- ( ( U e. NrmCVec /\ W e. H ) -> Y C_ X )

Proof

Step Hyp Ref Expression
1 sspba.x 
 |-  X = ( BaseSet ` U )
2 sspba.y 
 |-  Y = ( BaseSet ` W )
3 sspba.h 
 |-  H = ( SubSp ` U )
4 eqid 
 |-  ( +v ` U ) = ( +v ` U )
5 eqid 
 |-  ( +v ` W ) = ( +v ` W )
6 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
7 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
8 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
9 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
10 4 5 6 7 8 9 3 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 ) ) ) ) )
11 10 simplbda 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( +v ` W ) C_ ( +v ` U ) /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ ( normCV ` W ) C_ ( normCV ` U ) ) )
12 11 simp1d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( +v ` W ) C_ ( +v ` U ) )
13 rnss 
 |-  ( ( +v ` W ) C_ ( +v ` U ) -> ran ( +v ` W ) C_ ran ( +v ` U ) )
14 12 13 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ran ( +v ` W ) C_ ran ( +v ` U ) )
15 2 5 bafval 
 |-  Y = ran ( +v ` W )
16 1 4 bafval 
 |-  X = ran ( +v ` U )
17 14 15 16 3sstr4g 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ X )