This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )