Theorem diassdvaN

Description: The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	diassdva.b	|- B = ( Base ` K )
	diassdva.l	|- .<_ = ( le ` K )
	diassdva.h	|- H = ( LHyp ` K )
	diassdva.i	|- I = ( ( DIsoA ` K ) ` W )
	diassdva.u	|- U = ( ( DVecA ` K ) ` W )
	diassdva.v	|- V = ( Base ` U )
Assertion	diassdvaN	|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		diassdva.b	|- B = ( Base ` K )
2		diassdva.l	|- .<_ = ( le ` K )
3		diassdva.h	|- H = ( LHyp ` K )
4		diassdva.i	|- I = ( ( DIsoA ` K ) ` W )
5		diassdva.u	|- U = ( ( DVecA ` K ) ` W )
6		diassdva.v	|- V = ( Base ` U )
7		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
8		eqid	|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
9	1 2 3 7 8 4	diaval	|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } )
10		ssrab2	|- { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ ( ( LTrn ` K ) ` W )
11	3 7 5 6	dvavbase	|- ( ( K e. Y /\ W e. H ) -> V = ( ( LTrn ` K ) ` W ) )
12	11	adantr	|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> V = ( ( LTrn ` K ) ` W ) )
13	10 12	sseqtrrid	|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ V )
14	9 13	eqsstrd	|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )