| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dicelval1st.l |
|- .<_ = ( le ` K ) |
| 2 |
|
dicelval1st.a |
|- A = ( Atoms ` K ) |
| 3 |
|
dicelval1st.h |
|- H = ( LHyp ` K ) |
| 4 |
|
dicelval1st.t |
|- T = ( ( LTrn ` K ) ` W ) |
| 5 |
|
dicelval1st.i |
|- I = ( ( DIsoC ` K ) ` W ) |
| 6 |
|
eqid |
|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W ) |
| 7 |
|
eqid |
|- ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) ) |
| 8 |
1 2 3 5 6 7
|
dicssdvh |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) |
| 9 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
| 10 |
3 4 9 6 7
|
dvhvbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. ( ( TEndo ` K ) ` W ) ) ) |
| 11 |
10
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( T X. ( ( TEndo ` K ) ` W ) ) ) |
| 12 |
8 11
|
sseqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( T X. ( ( TEndo ` K ) ` W ) ) ) |
| 13 |
12
|
sseld |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) -> Y e. ( T X. ( ( TEndo ` K ) ` W ) ) ) ) |
| 14 |
13
|
3impia |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> Y e. ( T X. ( ( TEndo ` K ) ` W ) ) ) |
| 15 |
|
xp1st |
|- ( Y e. ( T X. ( ( TEndo ` K ) ` W ) ) -> ( 1st ` Y ) e. T ) |
| 16 |
14 15
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) e. T ) |