# Metamath Proof Explorer

## Theorem dihrnlss

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

Ref Expression
Hypotheses dihsslss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihsslss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihsslss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihsslss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion dihrnlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {X}\in {S}$

### Proof

Step Hyp Ref Expression
1 dihsslss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dihsslss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dihsslss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dihsslss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
5 1 2 3 4 dihsslss ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ran}{I}\subseteq {S}$
6 5 sselda ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {X}\in {S}$