Theorem dihrnss

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

	Ref	Expression
Hypotheses	dihrnss.h	|- H = ( LHyp ` K )
	dihrnss.u	|- U = ( ( DVecH ` K ) ` W )
	dihrnss.i	|- I = ( ( DIsoH ` K ) ` W )
	dihrnss.v	|- V = ( Base ` U )
Assertion	dihrnss	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ V )

Proof

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