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 ⊢ B = Base K
omlfh1.j ⊢ ∨ ˙ = join ⁡ K
omlfh1.m ⊢ ∧ ˙ = meet ⁡ K
omlfh1.c ⊢ C = cm ⁡ K
Assertion omlfh3N ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Y ∧ X C Z → X ∨ ˙ Y ∧ ˙ Z = X ∨ ˙ Y ∧ ˙ X ∨ ˙ Z

Proof

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