# 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}={\mathrm{Base}}_{{K}}$
lecmt.l
lecmt.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion lecmtN

### Proof

Step Hyp Ref Expression
1 lecmt.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lecmt.l
3 lecmt.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
4 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
5 4 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
6 simp2 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
7 omlop ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OP}$
8 7 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OP}$
9 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
10 1 9 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
11 8 6 10 syl2anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
12 simp3 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
13 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
14 1 13 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}$
15 5 11 12 14 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}$
16 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
17 1 2 16 latmle1
18 5 6 15 17 syl3anc
19 1 16 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\in {B}$
20 5 6 15 19 syl3anc ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\mathrm{meet}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right){Y}\right)\in {B}$
21 1 2 lattr
22 5 20 6 12 21 syl13anc
23 18 22 mpand
24 1 2 13 16 9 3 cmtbr4N
25 23 24 sylibrd