This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omlfh3N

Description: Foulis-Holland Theorem, part 3. Dual of omlfh1N . (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 omlfh3N ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )

Proof

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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑌 ∧ 𝑋 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )