Metamath Proof Explorer


Theorem dihrnlss

Description: The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dihsslss.h
|- H = ( LHyp ` K )
dihsslss.u
|- U = ( ( DVecH ` K ) ` W )
dihsslss.i
|- I = ( ( DIsoH ` K ) ` W )
dihsslss.s
|- S = ( LSubSp ` U )
Assertion dihrnlss
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. S )

Proof

Step Hyp Ref Expression
1 dihsslss.h
 |-  H = ( LHyp ` K )
2 dihsslss.u
 |-  U = ( ( DVecH ` K ) ` W )
3 dihsslss.i
 |-  I = ( ( DIsoH ` K ) ` W )
4 dihsslss.s
 |-  S = ( LSubSp ` U )
5 1 2 3 4 dihsslss
 |-  ( ( K e. HL /\ W e. H ) -> ran I C_ S )
6 5 sselda
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. S )