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