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 ) |
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 ) |