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=BaseK
cmtcom.c ⊢C=cm⁡K
Assertion cmtcomlemN ⊢K∈OML∧X∈B∧Y∈B→XCY→YCX

Proof

Step Hyp Ref Expression
1 cmtcom.b ⊢B=BaseK
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≤Koc⁡K⁡Xjoin⁡KY
14 4 9 10 13 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Y≤Koc⁡K⁡Xjoin⁡KY
15 1 12 latjcl ⊢K∈Lat∧oc⁡K⁡X∈B∧Y∈B→oc⁡K⁡Xjoin⁡KY∈B
16 4 9 10 15 syl3anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡KY∈B
17 eqid ⊢meet⁡K=meet⁡K
18 1 11 17 latleeqm2 ⊢K∈Lat∧Y∈B∧oc⁡K⁡Xjoin⁡KY∈B→Y≤Koc⁡K⁡Xjoin⁡KY↔oc⁡K⁡Xjoin⁡KYmeet⁡KY=Y
19 4 10 16 18 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Y≤Koc⁡K⁡Xjoin⁡KY↔oc⁡K⁡Xjoin⁡KYmeet⁡KY=Y
20 14 19 mpbid ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡KYmeet⁡KY=Y
21 20 oveq2d ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡KY
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⁡Xjoin⁡Koc⁡K⁡Y∈B
28 4 9 26 27 syl3anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B
29 1 17 latmassOLD ⊢K∈OL∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B∧oc⁡K⁡Xjoin⁡KY∈B∧Y∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY
30 23 28 16 10 29 syl13anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY
31 1 12 17 6 oldmm1 ⊢K∈OL∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Y
32 22 31 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Y
33 32 oveq1d ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡KY
34 21 30 33 3eqtr4rd ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY
35 34 adantr ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡Xmeet⁡KYmeet⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY
36 1 12 17 6 oldmj4 ⊢K∈OL∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y=Xmeet⁡KY
37 22 36 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y=Xmeet⁡KY
38 1 12 17 6 oldmj2 ⊢K∈OL∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡KY=Xmeet⁡Koc⁡K⁡Y
39 22 38 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡KY=Xmeet⁡Koc⁡K⁡Y
40 37 39 oveq12d ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y
41 40 eqeq2d ⊢K∈OML∧X∈B∧Y∈B→X=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY↔X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y
42 41 biimpar ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→X=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY
43 42 fveq2d ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡X=oc⁡K⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY
44 1 12 17 6 oldmj4 ⊢K∈OL∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B∧oc⁡K⁡Xjoin⁡KY∈B→oc⁡K⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KY
45 23 28 16 44 syl3anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KY
46 45 adantr ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡oc⁡K⁡Xjoin⁡KY=oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KY
47 43 46 eqtr2d ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KY=oc⁡K⁡X
48 47 oveq1d ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡Xjoin⁡Koc⁡K⁡Ymeet⁡Koc⁡K⁡Xjoin⁡KYmeet⁡KY=oc⁡K⁡Xmeet⁡KY
49 35 48 eqtrd ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→oc⁡K⁡Xmeet⁡KYmeet⁡KY=oc⁡K⁡Xmeet⁡KY
50 49 oveq2d ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KYmeet⁡KY=Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KY
51 simp1 ⊢K∈OML∧X∈B∧Y∈B→K∈OML
52 1 17 latmcl ⊢K∈Lat∧X∈B∧Y∈B→Xmeet⁡KY∈B
53 3 52 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KY∈B
54 51 53 10 3jca ⊢K∈OML∧X∈B∧Y∈B→K∈OML∧Xmeet⁡KY∈B∧Y∈B
55 1 11 17 latmle2 ⊢K∈Lat∧X∈B∧Y∈B→Xmeet⁡KY≤KY
56 3 55 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KY≤KY
57 1 11 12 17 6 omllaw2N ⊢K∈OML∧Xmeet⁡KY∈B∧Y∈B→Xmeet⁡KY≤KY→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KYmeet⁡KY=Y
58 54 56 57 sylc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KYmeet⁡KY=Y
59 58 adantr ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KYmeet⁡KY=Y
60 1 17 latmcom ⊢K∈Lat∧X∈B∧Y∈B→Xmeet⁡KY=Ymeet⁡KX
61 3 60 syl3an1 ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KY=Ymeet⁡KX
62 1 17 latmcom ⊢K∈Lat∧oc⁡K⁡X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KY=Ymeet⁡Koc⁡K⁡X
63 4 9 10 62 syl3anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡KY=Ymeet⁡Koc⁡K⁡X
64 61 63 oveq12d ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KY=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
65 64 adantr ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→Xmeet⁡KYjoin⁡Koc⁡K⁡Xmeet⁡KY=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
66 50 59 65 3eqtr3d ⊢K∈OML∧X∈B∧Y∈B∧X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→Y=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
67 66 ex ⊢K∈OML∧X∈B∧Y∈B→X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y→Y=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
68 1 12 17 6 2 cmtvalN ⊢K∈OML∧X∈B∧Y∈B→XCY↔X=Xmeet⁡KYjoin⁡KXmeet⁡Koc⁡K⁡Y
69 1 12 17 6 2 cmtvalN ⊢K∈OML∧Y∈B∧X∈B→YCX↔Y=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
70 69 3com23 ⊢K∈OML∧X∈B∧Y∈B→YCX↔Y=Ymeet⁡KXjoin⁡KYmeet⁡Koc⁡K⁡X
71 67 68 70 3imtr4d ⊢K∈OML∧X∈B∧Y∈B→XCY→YCX