Step |
Hyp |
Ref |
Expression |
1 |
|
dihmeetlem7.b |
|- B = ( Base ` K ) |
2 |
|
dihmeetlem7.l |
|- .<_ = ( le ` K ) |
3 |
|
dihmeetlem7.j |
|- .\/ = ( join ` K ) |
4 |
|
dihmeetlem7.m |
|- ./\ = ( meet ` K ) |
5 |
|
dihmeetlem7.a |
|- A = ( Atoms ` K ) |
6 |
|
simprr |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> -. p .<_ Y ) |
7 |
|
simpl1 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> K e. HL ) |
8 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
9 |
7 8
|
syl |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> K e. AtLat ) |
10 |
|
simprl |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> p e. A ) |
11 |
|
simpl3 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> Y e. B ) |
12 |
|
eqid |
|- ( 0. ` K ) = ( 0. ` K ) |
13 |
1 2 4 12 5
|
atnle |
|- ( ( K e. AtLat /\ p e. A /\ Y e. B ) -> ( -. p .<_ Y <-> ( p ./\ Y ) = ( 0. ` K ) ) ) |
14 |
9 10 11 13
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( -. p .<_ Y <-> ( p ./\ Y ) = ( 0. ` K ) ) ) |
15 |
6 14
|
mpbid |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( p ./\ Y ) = ( 0. ` K ) ) |
16 |
15
|
oveq2d |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( ( X ./\ Y ) .\/ ( p ./\ Y ) ) = ( ( X ./\ Y ) .\/ ( 0. ` K ) ) ) |
17 |
7
|
hllatd |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> K e. Lat ) |
18 |
|
simpl2 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> X e. B ) |
19 |
1 4
|
latmcl |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B ) |
20 |
17 18 11 19
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( X ./\ Y ) e. B ) |
21 |
1 2 4
|
latmle2 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y ) |
22 |
17 18 11 21
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( X ./\ Y ) .<_ Y ) |
23 |
1 2 3 4 5
|
atmod1i2 |
|- ( ( K e. HL /\ ( p e. A /\ ( X ./\ Y ) e. B /\ Y e. B ) /\ ( X ./\ Y ) .<_ Y ) -> ( ( X ./\ Y ) .\/ ( p ./\ Y ) ) = ( ( ( X ./\ Y ) .\/ p ) ./\ Y ) ) |
24 |
7 10 20 11 22 23
|
syl131anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( ( X ./\ Y ) .\/ ( p ./\ Y ) ) = ( ( ( X ./\ Y ) .\/ p ) ./\ Y ) ) |
25 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
26 |
7 25
|
syl |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> K e. OL ) |
27 |
1 3 12
|
olj01 |
|- ( ( K e. OL /\ ( X ./\ Y ) e. B ) -> ( ( X ./\ Y ) .\/ ( 0. ` K ) ) = ( X ./\ Y ) ) |
28 |
26 20 27
|
syl2anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( ( X ./\ Y ) .\/ ( 0. ` K ) ) = ( X ./\ Y ) ) |
29 |
16 24 28
|
3eqtr3d |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( p e. A /\ -. p .<_ Y ) ) -> ( ( ( X ./\ Y ) .\/ p ) ./\ Y ) = ( X ./\ Y ) ) |