Metamath Proof Explorer

Theorem omlfh1N

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omlfh1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
omlfh1.j ⊢ ∨ = ( join ‘ 𝐾 )
omlfh1.m ⊢ ∧ = ( meet ‘ 𝐾 )
omlfh1.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion omlfh1N ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 omlfh1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omlfh1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 omlfh1.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 omlfh1.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
5 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 1 6 2 3 latledi ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
8 5 7 sylan ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
9 8 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
10 5 adantr ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
11 simpr1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
12 simpr2 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
13 simpr3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
14 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
15 10 12 13 14 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
16 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) )
17 10 11 15 16 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) )
18 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
19 18 adantr ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OL )
20 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
21 10 11 12 20 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
22 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
23 10 11 13 22 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
24 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
25 1 2 3 24 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑍 ) ) ) )
26 19 21 23 25 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑍 ) ) ) )
27 1 2 3 24 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
28 19 11 12 27 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
29 1 2 3 24 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑍 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
30 19 11 13 29 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑍 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
31 28 30 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑌 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑍 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
32 26 31 eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
33 17 32 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
34 33 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
35 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
36 35 adantr ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OP )
37 1 24 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
38 36 11 37 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
39 1 24 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
40 36 12 39 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
41 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
42 10 38 40 41 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
43 1 24 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 )
44 36 13 43 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 )
45 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 )
46 10 38 44 45 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 )
47 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ∈ 𝐵 )
48 10 42 46 47 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ∈ 𝐵 )
49 1 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ∈ 𝐵 ) ) → ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) )
50 19 15 11 48 49 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) )
51 50 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) )
52 1 24 4 cmt2N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
53 52 3adant3r3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
54 simpl ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ OML )
55 1 2 3 24 4 cmtbr3N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
56 54 11 40 55 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
57 53 56 bitrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
58 57 biimpa ⊢ ( ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
59 58 adantrr ⊢ ( ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
60 59 3impa ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
61 1 24 4 cmt2N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑍 ↔ 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
62 61 3adant3r2 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑍 ↔ 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
63 1 2 3 24 4 cmtbr3N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
64 54 11 44 63 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
65 62 64 bitrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑍 ↔ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
66 65 biimpa ⊢ ( ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑍 ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
67 66 adantrl ⊢ ( ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
68 67 3impa ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
69 60 68 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
70 1 3 latmmdiN ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
71 19 11 42 46 70 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
72 71 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
73 1 3 latmmdiN ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
74 19 11 40 44 73 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
75 74 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( 𝑋 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
76 69 72 75 3eqtr4d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
77 76 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
78 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 )
79 10 40 44 78 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 )
80 1 3 latm12 ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ∈ 𝐵 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
81 19 15 11 79 80 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
82 81 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( 𝑋 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
83 51 77 82 3eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( ( 𝑌 ∨ 𝑍 ) ∧ 𝑋 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) )
84 1 2 3 24 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∨ 𝑍 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
85 19 12 13 84 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∨ 𝑍 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) )
86 85 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∨ 𝑍 ) ) ) = ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) )
87 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
88 1 24 3 87 opnoncon ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∨ 𝑍 ) ) ) = ( 0. ‘ 𝐾 ) )
89 36 15 88 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∨ 𝑍 ) ) ) = ( 0. ‘ 𝐾 ) )
90 86 89 eqtr3d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) = ( 0. ‘ 𝐾 ) )
91 90 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 𝑋 ∧ ( 0. ‘ 𝐾 ) ) )
92 1 3 87 olm01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ ( 0. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
93 19 11 92 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( 0. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
94 91 93 eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) )
95 94 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑍 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) )
96 34 83 95 3eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) )
97 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 )
98 10 21 23 97 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 )
99 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 )
100 10 11 15 99 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 )
101 1 6 3 24 87 omllaw3 ⊢ ( ( 𝐾 ∈ OML ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 ∧ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∈ 𝐵 ) → ( ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )
102 54 98 100 101 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )
103 102 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ) ) = ( 0. ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )
104 9 96 103 mp2and ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) = ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
105 104 eqcomd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) )