Step |
Hyp |
Ref |
Expression |
1 |
|
dihglbc.b |
|- B = ( Base ` K ) |
2 |
|
dihglbc.g |
|- G = ( glb ` K ) |
3 |
|
dihglbc.h |
|- H = ( LHyp ` K ) |
4 |
|
dihglbc.i |
|- I = ( ( DIsoH ` K ) ` W ) |
5 |
|
dihglbc.l |
|- .<_ = ( le ` K ) |
6 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
7 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
8 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
9 |
|
eqid |
|- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W ) |
10 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
11 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
12 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
13 |
|
eqid |
|- ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = q ) = ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = q ) |
14 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
dihglbcpreN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) ) |