Theorem dihss

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

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

Proof

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