Step |
Hyp |
Ref |
Expression |
1 |
|
dihord3.b |
|- B = ( Base ` K ) |
2 |
|
dihord3.l |
|- .<_ = ( le ` K ) |
3 |
|
dihord3.h |
|- H = ( LHyp ` K ) |
4 |
|
dihord3.i |
|- I = ( ( DIsoH ` K ) ` W ) |
5 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
6 |
|
eqid |
|- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W ) |
7 |
|
eqid |
|- ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) |
8 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
9 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
10 |
|
eqid |
|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W ) |
11 |
|
eqid |
|- ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) ) |
12 |
|
eqid |
|- ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = q ) = ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = q ) |
13 |
1 2 5 3 6 7 8 9 4 10 11 12
|
dihord6apre |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y ) |