| Step |
Hyp |
Ref |
Expression |
| 1 |
|
omlfh1.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
omlfh1.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
| 3 |
|
omlfh1.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
| 4 |
|
omlfh1.c |
⊢ 𝐶 = ( cm ‘ 𝐾 ) |
| 5 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
| 6 |
1 5 4
|
cmt4N |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 7 |
6
|
3adant3r3 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) |
| 8 |
1 5 4
|
cmt4N |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) |
| 9 |
8
|
3adant3r2 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) |
| 10 |
7 9
|
anbi12d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) |
| 11 |
|
simpl |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OML ) |
| 12 |
|
omlop |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP ) |
| 13 |
12
|
adantr |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OP ) |
| 14 |
|
simpr1 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 ) |
| 15 |
1 5
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 16 |
13 14 15
|
syl2anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) |
| 17 |
|
simpr2 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 ) |
| 18 |
1 5
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 19 |
13 17 18
|
syl2anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) |
| 20 |
|
simpr3 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 ) |
| 21 |
1 5
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) |
| 22 |
13 20 21
|
syl2anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) |
| 23 |
16 19 22
|
3jca |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ) |
| 24 |
1 2 3 4
|
omlfh1N |
⊢ ( ( 𝐾 ∈ OML ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) |
| 25 |
24
|
fveq2d |
⊢ ( ( 𝐾 ∈ OML ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 26 |
25
|
3exp |
⊢ ( 𝐾 ∈ OML → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) ) ) |
| 27 |
11 23 26
|
sylc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) ) |
| 28 |
10 27
|
sylbid |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) ) |
| 29 |
28
|
3impia |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 30 |
|
omlol |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL ) |
| 31 |
30
|
adantr |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OL ) |
| 32 |
|
omllat |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat ) |
| 33 |
32
|
adantr |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat ) |
| 34 |
1 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) |
| 35 |
33 19 22 34
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) |
| 36 |
1 2 3 5
|
oldmm2 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∨ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 37 |
31 14 35 36
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∨ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 38 |
1 2 3 5
|
oldmj4 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑌 ∧ 𝑍 ) ) |
| 39 |
31 17 20 38
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑌 ∧ 𝑍 ) ) |
| 40 |
39
|
oveq2d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) |
| 41 |
37 40
|
eqtr2d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 42 |
41
|
3adant3 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 43 |
1 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) |
| 44 |
33 16 19 43
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) |
| 45 |
1 3
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) |
| 46 |
33 16 22 45
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) |
| 47 |
1 2 3 5
|
oldmj1 |
⊢ ( ( 𝐾 ∈ OL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 48 |
31 44 46 47
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 49 |
1 2 3 5
|
oldmm4 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) ) |
| 50 |
31 14 17 49
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) ) |
| 51 |
1 2 3 5
|
oldmm4 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∨ 𝑍 ) ) |
| 52 |
31 14 20 51
|
syl3anc |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∨ 𝑍 ) ) |
| 53 |
50 52
|
oveq12d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) ) |
| 54 |
48 53
|
eqtr2d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 55 |
54
|
3adant3 |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) |
| 56 |
29 42 55
|
3eqtr4d |
⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) ) |