Step |
Hyp |
Ref |
Expression |
1 |
|
omllaw4.b |
|- B = ( Base ` K ) |
2 |
|
omllaw4.l |
|- .<_ = ( le ` K ) |
3 |
|
omllaw4.m |
|- ./\ = ( meet ` K ) |
4 |
|
omllaw4.o |
|- ._|_ = ( oc ` K ) |
5 |
|
simp1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML ) |
6 |
|
omlop |
|- ( K e. OML -> K e. OP ) |
7 |
6
|
3ad2ant1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP ) |
8 |
|
simp3 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B ) |
9 |
1 4
|
opoccl |
|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B ) |
10 |
7 8 9
|
syl2anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B ) |
11 |
|
simp2 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B ) |
12 |
1 4
|
opoccl |
|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B ) |
13 |
7 11 12
|
syl2anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B ) |
14 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
15 |
1 2 14 3 4
|
omllaw |
|- ( ( K e. OML /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` X ) e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) ) |
16 |
5 10 13 15
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) ) |
17 |
1 2 4
|
oplecon3b |
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) |
18 |
6 17
|
syl3an1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) |
19 |
|
omllat |
|- ( K e. OML -> K e. Lat ) |
20 |
19
|
3ad2ant1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat ) |
21 |
1 3
|
latmcl |
|- ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) e. B ) |
22 |
20 13 8 21
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) e. B ) |
23 |
1 4
|
opoccl |
|- ( ( K e. OP /\ ( ( ._|_ ` X ) ./\ Y ) e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B ) |
24 |
7 22 23
|
syl2anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B ) |
25 |
1 3
|
latmcl |
|- ( ( K e. Lat /\ ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B /\ Y e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B ) |
26 |
20 24 8 25
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B ) |
27 |
1 4
|
opcon3b |
|- ( ( K e. OP /\ ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B /\ X e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) ) ) |
28 |
7 26 11 27
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) ) ) |
29 |
1 14
|
latjcom |
|- ( ( K e. Lat /\ ( ( ._|_ ` X ) ./\ Y ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) ) |
30 |
20 22 10 29
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) ) |
31 |
|
omlol |
|- ( K e. OML -> K e. OL ) |
32 |
31
|
3ad2ant1 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OL ) |
33 |
1 14 3 4
|
oldmm2 |
|- ( ( K e. OL /\ ( ( ._|_ ` X ) ./\ Y ) e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) ) |
34 |
32 22 8 33
|
syl3anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) ) |
35 |
1 4
|
opococ |
|- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y ) |
36 |
7 8 35
|
syl2anc |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y ) |
37 |
36
|
oveq2d |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) ./\ Y ) ) |
38 |
37
|
oveq2d |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) ) |
39 |
30 34 38
|
3eqtr4d |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) |
40 |
39
|
eqeq2d |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) <-> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) ) |
41 |
28 40
|
bitrd |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) ) |
42 |
16 18 41
|
3imtr4d |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X ) ) |