| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cmtcom.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
cmtcom.c |
⊢ 𝐶 = ( cm ‘ 𝐾 ) |
| 3 |
|
omllat |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat ) |
| 4 |
3
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat ) |
| 5 |
|
omlop |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP ) |
| 6 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
| 7 |
1 6
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 8 |
5 7
|
sylan |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 9 |
8
|
3adant3 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 10 |
|
simp3 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 ) |
| 11 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 12 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 13 |
1 11 12
|
latlej2 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) |
| 14 |
4 9 10 13
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) |
| 15 |
1 12
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) |
| 16 |
4 9 10 15
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) |
| 17 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
| 18 |
1 11 17
|
latleeqm2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) → ( 𝑌 ( le ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ↔ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) = 𝑌 ) ) |
| 19 |
4 10 16 18
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ( le ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ↔ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) = 𝑌 ) ) |
| 20 |
14 19
|
mpbid |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) = 𝑌 ) |
| 21 |
20
|
oveq2d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 22 |
|
omlol |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL ) |
| 23 |
22
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OL ) |
| 24 |
5
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP ) |
| 25 |
1 6
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 26 |
24 10 25
|
syl2anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 27 |
1 12
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) |
| 28 |
4 9 26 27
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) |
| 29 |
1 17
|
latmassOLD |
⊢ ( ( 𝐾 ∈ OL ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) ) ) |
| 30 |
23 28 16 10 29
|
syl13anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ( meet ‘ 𝐾 ) 𝑌 ) ) ) |
| 31 |
1 12 17 6
|
oldmm1 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 32 |
22 31
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 33 |
32
|
oveq1d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 34 |
21 30 33
|
3eqtr4rd |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 35 |
34
|
adantr |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 36 |
1 12 17 6
|
oldmj4 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 37 |
22 36
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 38 |
1 12 17 6
|
oldmj2 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) = ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 39 |
22 38
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) = ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 40 |
37 39
|
oveq12d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) |
| 41 |
40
|
eqeq2d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ↔ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) ) |
| 42 |
41
|
biimpar |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑋 = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ) |
| 43 |
42
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ) ) |
| 44 |
1 12 17 6
|
oldmj4 |
⊢ ( ( 𝐾 ∈ OL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) |
| 45 |
23 28 16 44
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) |
| 46 |
45
|
adantr |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ) |
| 47 |
43 46
|
eqtr2d |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) |
| 48 |
47
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 49 |
35 48
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) ) |
| 50 |
49
|
oveq2d |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) ) ) |
| 51 |
|
simp1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML ) |
| 52 |
1 17
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) |
| 53 |
3 52
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) |
| 54 |
51 53 10
|
3jca |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 ∈ OML ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) |
| 55 |
1 11 17
|
latmle2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) |
| 56 |
3 55
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) |
| 57 |
1 11 12 17 6
|
omllaw2N |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( le ‘ 𝐾 ) 𝑌 → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) = 𝑌 ) ) |
| 58 |
54 56 57
|
sylc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) = 𝑌 ) |
| 59 |
58
|
adantr |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) ( meet ‘ 𝐾 ) 𝑌 ) ) = 𝑌 ) |
| 60 |
1 17
|
latmcom |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) = ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ) |
| 61 |
3 60
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) = ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ) |
| 62 |
1 17
|
latmcom |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) = ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 63 |
4 9 10 62
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) = ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) |
| 64 |
61 63
|
oveq12d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) |
| 65 |
64
|
adantr |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) 𝑌 ) ) = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) |
| 66 |
50 59 65
|
3eqtr3d |
⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑌 = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) |
| 67 |
66
|
ex |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) → 𝑌 = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
| 68 |
1 12 17 6 2
|
cmtvalN |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 = ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) ) |
| 69 |
1 12 17 6 2
|
cmtvalN |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
| 70 |
69
|
3com23 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 = ( ( 𝑌 ( meet ‘ 𝐾 ) 𝑋 ) ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
| 71 |
67 68 70
|
3imtr4d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑌 𝐶 𝑋 ) ) |