| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dihvalb.b |
|- B = ( Base ` K ) |
| 2 |
|
dihvalb.l |
|- .<_ = ( le ` K ) |
| 3 |
|
dihvalb.h |
|- H = ( LHyp ` K ) |
| 4 |
|
dihvalb.i |
|- I = ( ( DIsoH ` K ) ` W ) |
| 5 |
|
dihvalb.d |
|- D = ( ( DIsoB ` K ) ` W ) |
| 6 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
| 7 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
| 8 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
| 9 |
|
eqid |
|- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W ) |
| 10 |
|
eqid |
|- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W ) |
| 11 |
|
eqid |
|- ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) ) |
| 12 |
|
eqid |
|- ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) ) |
| 13 |
1 2 6 7 8 3 4 5 9 10 11 12
|
dihval |
|- ( ( ( K e. V /\ W e. H ) /\ X e. B ) -> ( I ` X ) = if ( X .<_ W , ( D ` X ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) A. q e. ( Atoms ` K ) ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( D ` ( X ( meet ` K ) W ) ) ) ) ) ) ) |
| 14 |
|
iftrue |
|- ( X .<_ W -> if ( X .<_ W , ( D ` X ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) A. q e. ( Atoms ` K ) ( ( -. q .<_ W /\ ( q ( join ` K ) ( X ( meet ` K ) W ) ) = X ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( D ` ( X ( meet ` K ) W ) ) ) ) ) ) = ( D ` X ) ) |
| 15 |
13 14
|
sylan9eq |
|- ( ( ( ( K e. V /\ W e. H ) /\ X e. B ) /\ X .<_ W ) -> ( I ` X ) = ( D ` X ) ) |
| 16 |
15
|
anasss |
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( D ` X ) ) |