Theorem dihrnss

Description: The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014)

	Ref	Expression
Hypotheses	dihrnss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihrnss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihrnss.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihrnss.v	$$⊢V={\mathrm{Base}}_U$$
Assertion	dihrnss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to X\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		dihrnss.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dihrnss.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dihrnss.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		dihrnss.v	$$⊢V={\mathrm{Base}}_U$$
5		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
6	1 2 3 5	dihrnlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to X\in \mathrm{LSubSp}\left(U\right)$$
7	4 5	lssss	$$⊢X\in \mathrm{LSubSp}\left(U\right)\to X\subseteq V$$
8	6 7	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to X\subseteq V$$