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