Metamath Proof Explorer

Theorem cmtcomlemN

Description: Lemma for cmtcomN . ( cmcmlem analog.) (Contributed by NM, 7-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtcom.b ⊢ B = Base K
cmtcom.c ⊢ C = cm ⁡ K
Assertion cmtcomlemN ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y → Y C X

Proof

Step Hyp Ref Expression
1 cmtcom.b ⊢ B = Base K
2 cmtcom.c ⊢ C = cm ⁡ K
3 omllat ⊢ K ∈ OML → K ∈ Lat
4 3 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ Lat
5 omlop ⊢ K ∈ OML → K ∈ OP
6 eqid ⊢ oc ⁡ K = oc ⁡ K
7 1 6 opoccl ⊢ K ∈ OP ∧ X ∈ B → oc ⁡ K ⁡ X ∈ B
8 5 7 sylan ⊢ K ∈ OML ∧ X ∈ B → oc ⁡ K ⁡ X ∈ B
9 8 3adant3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X ∈ B
10 simp3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 eqid ⊢ join ⁡ K = join ⁡ K
13 1 11 12 latlej2 ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X ∈ B ∧ Y ∈ B → Y ≤ K oc ⁡ K ⁡ X join ⁡ K Y
14 4 9 10 13 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y ≤ K oc ⁡ K ⁡ X join ⁡ K Y
15 1 12 latjcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K Y ∈ B
16 4 9 10 15 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K Y ∈ B
17 eqid ⊢ meet ⁡ K = meet ⁡ K
18 1 11 17 latleeqm2 ⊢ K ∈ Lat ∧ Y ∈ B ∧ oc ⁡ K ⁡ X join ⁡ K Y ∈ B → Y ≤ K oc ⁡ K ⁡ X join ⁡ K Y ↔ oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = Y
19 4 10 16 18 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y ≤ K oc ⁡ K ⁡ X join ⁡ K Y ↔ oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = Y
20 14 19 mpbid ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = Y
21 20 oveq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K Y
22 omlol ⊢ K ∈ OML → K ∈ OL
23 22 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OL
24 5 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OP
25 1 6 opoccl ⊢ K ∈ OP ∧ Y ∈ B → oc ⁡ K ⁡ Y ∈ B
26 24 10 25 syl2anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ Y ∈ B
27 1 12 latjcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X ∈ B ∧ oc ⁡ K ⁡ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B
28 4 9 26 27 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B
29 1 17 latmassOLD ⊢ K ∈ OL ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B ∧ oc ⁡ K ⁡ X join ⁡ K Y ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y
30 23 28 16 10 29 syl13anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y
31 1 12 17 6 oldmm1 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y
32 22 31 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y
33 32 oveq1d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K Y
34 21 30 33 3eqtr4rd ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y
35 34 adantr ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y
36 1 12 17 6 oldmj4 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y = X meet ⁡ K Y
37 22 36 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y = X meet ⁡ K Y
38 1 12 17 6 oldmj2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = X meet ⁡ K oc ⁡ K ⁡ Y
39 22 38 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = X meet ⁡ K oc ⁡ K ⁡ Y
40 37 39 oveq12d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y
41 40 eqeq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X = oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y ↔ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y
42 41 biimpar ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → X = oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y
43 42 fveq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ X = oc ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y
44 1 12 17 6 oldmj4 ⊢ K ∈ OL ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B ∧ oc ⁡ K ⁡ X join ⁡ K Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y
45 23 28 16 44 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y
46 45 adantr ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K Y = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y
47 43 46 eqtr2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y = oc ⁡ K ⁡ X
48 47 oveq1d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y meet ⁡ K oc ⁡ K ⁡ X join ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X meet ⁡ K Y
49 35 48 eqtrd ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = oc ⁡ K ⁡ X meet ⁡ K Y
50 49 oveq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y
51 simp1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OML
52 1 17 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
53 3 52 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
54 51 53 10 3jca ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OML ∧ X meet ⁡ K Y ∈ B ∧ Y ∈ B
55 1 11 17 latmle2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ≤ K Y
56 3 55 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ≤ K Y
57 1 11 12 17 6 omllaw2N ⊢ K ∈ OML ∧ X meet ⁡ K Y ∈ B ∧ Y ∈ B → X meet ⁡ K Y ≤ K Y → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = Y
58 54 56 57 sylc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = Y
59 58 adantr ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y meet ⁡ K Y = Y
60 1 17 latmcom ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y = Y meet ⁡ K X
61 3 60 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y = Y meet ⁡ K X
62 1 17 latmcom ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y = Y meet ⁡ K oc ⁡ K ⁡ X
63 4 9 10 62 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K Y = Y meet ⁡ K oc ⁡ K ⁡ X
64 61 63 oveq12d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
65 64 adantr ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → X meet ⁡ K Y join ⁡ K oc ⁡ K ⁡ X meet ⁡ K Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
66 50 59 65 3eqtr3d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
67 66 ex ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y → Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
68 1 12 17 6 2 cmtvalN ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K oc ⁡ K ⁡ Y
69 1 12 17 6 2 cmtvalN ⊢ K ∈ OML ∧ Y ∈ B ∧ X ∈ B → Y C X ↔ Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
70 69 3com23 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y C X ↔ Y = Y meet ⁡ K X join ⁡ K Y meet ⁡ K oc ⁡ K ⁡ X
71 67 68 70 3imtr4d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y → Y C X