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

Proof

Step Hyp Ref Expression
1 omlfh1.b ⊢B=BaseK
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→XCY↔oc⁡K⁡XCoc⁡K⁡Y
7 6 3adant3r3 ⊢K∈OML∧X∈B∧Y∈B∧Z∈B→XCY↔oc⁡K⁡XCoc⁡K⁡Y
8 1 5 4 cmt4N ⊢K∈OML∧X∈B∧Z∈B→XCZ↔oc⁡K⁡XCoc⁡K⁡Z
9 8 3adant3r2 ⊢K∈OML∧X∈B∧Y∈B∧Z∈B→XCZ↔oc⁡K⁡XCoc⁡K⁡Z
10 7 9 anbi12d ⊢K∈OML∧X∈B∧Y∈B∧Z∈B→XCY∧XCZ↔oc⁡K⁡XCoc⁡K⁡Y∧oc⁡K⁡XCoc⁡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⁡XCoc⁡K⁡Y∧oc⁡K⁡XCoc⁡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⁡XCoc⁡K⁡Y∧oc⁡K⁡XCoc⁡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⁡XCoc⁡K⁡Y∧oc⁡K⁡XCoc⁡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⁡XCoc⁡K⁡Y∧oc⁡K⁡XCoc⁡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→XCY∧XCZ→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∧XCY∧XCZ→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∧XCY∧XCZ→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∧XCY∧XCZ→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∧XCY∧XCZ→X∨˙Y∧˙Z=X∨˙Y∧˙X∨˙Z