Metamath Proof Explorer

Theorem lecmtN

Description: Ordered elements commute. ( lecmi analog.) (Contributed by NM, 10-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses lecmt.b ⊢B=BaseK
lecmt.l ⊢≤˙=≤K
lecmt.c ⊢C=cm⁡K
Assertion lecmtN ⊢K∈OML∧X∈B∧Y∈B→X≤˙Y→XCY

Proof

Step Hyp Ref Expression
1 lecmt.b ⊢B=BaseK
2 lecmt.l ⊢≤˙=≤K
3 lecmt.c ⊢C=cm⁡K
4 omllat ⊢K∈OML→K∈Lat
5 4 3ad2ant1 ⊢K∈OML∧X∈B∧Y∈B→K∈Lat
6 simp2 ⊢K∈OML∧X∈B∧Y∈B→X∈B
7 omlop ⊢K∈OML→K∈OP
8 7 3ad2ant1 ⊢K∈OML∧X∈B∧Y∈B→K∈OP
9 eqid ⊢oc⁡K=oc⁡K
10 1 9 opoccl ⊢K∈OP∧X∈B→oc⁡K⁡X∈B
11 8 6 10 syl2anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡X∈B
12 simp3 ⊢K∈OML∧X∈B∧Y∈B→Y∈B
13 eqid ⊢join⁡K=join⁡K
14 1 13 latjcl ⊢K∈Lat∧oc⁡K⁡X∈B∧Y∈B→oc⁡K⁡Xjoin⁡KY∈B
15 5 11 12 14 syl3anc ⊢K∈OML∧X∈B∧Y∈B→oc⁡K⁡Xjoin⁡KY∈B
16 eqid ⊢meet⁡K=meet⁡K
17 1 2 16 latmle1 ⊢K∈Lat∧X∈B∧oc⁡K⁡Xjoin⁡KY∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙X
18 5 6 15 17 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙X
19 1 16 latmcl ⊢K∈Lat∧X∈B∧oc⁡K⁡Xjoin⁡KY∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY∈B
20 5 6 15 19 syl3anc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY∈B
21 1 2 lattr ⊢K∈Lat∧Xmeet⁡Koc⁡K⁡Xjoin⁡KY∈B∧X∈B∧Y∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙X∧X≤˙Y→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙Y
22 5 20 6 12 21 syl13anc ⊢K∈OML∧X∈B∧Y∈B→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙X∧X≤˙Y→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙Y
23 18 22 mpand ⊢K∈OML∧X∈B∧Y∈B→X≤˙Y→Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙Y
24 1 2 13 16 9 3 cmtbr4N ⊢K∈OML∧X∈B∧Y∈B→XCY↔Xmeet⁡Koc⁡K⁡Xjoin⁡KY≤˙Y
25 23 24 sylibrd ⊢K∈OML∧X∈B∧Y∈B→X≤˙Y→XCY