Theorem dihssxp

Description: An isomorphism H value is included in the vector space (expressed as T X. E ). (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dihssxp.b	|- B = ( Base ` K )
	dihssxp.h	|- H = ( LHyp ` K )
	dihssxp.t	|- T = ( ( LTrn ` K ) ` W )
	dihssxp.e	|- E = ( ( TEndo ` K ) ` W )
	dihssxp.i	|- I = ( ( DIsoH ` K ) ` W )
	dihssxp.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihssxp.x	|- ( ph -> X e. B )
Assertion	dihssxp	|- ( ph -> ( I ` X ) C_ ( T X. E ) )

Proof

Step	Hyp	Ref	Expression
1		dihssxp.b	|- B = ( Base ` K )
2		dihssxp.h	|- H = ( LHyp ` K )
3		dihssxp.t	|- T = ( ( LTrn ` K ) ` W )
4		dihssxp.e	|- E = ( ( TEndo ` K ) ` W )
5		dihssxp.i	|- I = ( ( DIsoH ` K ) ` W )
6		dihssxp.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dihssxp.x	|- ( ph -> X e. B )
8		eqid	|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
9		eqid	|- ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
10	1 2 5 8 9	dihss	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
11	6 7 10	syl2anc	|- ( ph -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
12	2 3 4 8 9	dvhvbase	|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. E ) )
13	6 12	syl	|- ( ph -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. E ) )
14	11 13	sseqtrd	|- ( ph -> ( I ` X ) C_ ( T X. E ) )