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