| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ltrnldil.h |
|- H = ( LHyp ` K ) |
| 2 |
|
ltrnldil.d |
|- D = ( ( LDil ` K ) ` W ) |
| 3 |
|
ltrnldil.t |
|- T = ( ( LTrn ` K ) ` W ) |
| 4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
| 5 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
| 6 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
| 7 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
| 8 |
4 5 6 7 1 2 3
|
isltrn |
|- ( ( K e. V /\ W e. H ) -> ( F e. T <-> ( F e. D /\ A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) ( ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) -> ( ( p ( join ` K ) ( F ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( F ` q ) ) ( meet ` K ) W ) ) ) ) ) |
| 9 |
8
|
simprbda |
|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. D ) |