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 = ( Base ` K )
	dihss.h	|- H = ( LHyp ` K )
	dihss.i	|- I = ( ( DIsoH ` K ) ` W )
	dihss.u	|- U = ( ( DVecH ` K ) ` W )
	dihss.v	|- V = ( Base ` U )
Assertion	dihss	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		dihss.b	|- B = ( Base ` K )
2		dihss.h	|- H = ( LHyp ` K )
3		dihss.i	|- I = ( ( DIsoH ` K ) ` W )
4		dihss.u	|- U = ( ( DVecH ` K ) ` W )
5		dihss.v	|- V = ( Base ` U )
6		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
7	1 2 3 4 6	dihlss	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ( LSubSp ` U ) )
8	5 6	lssss	|- ( ( I ` X ) e. ( LSubSp ` U ) -> ( I ` X ) C_ V )
9	7 8	syl	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) C_ V )