# 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 = ( Base ` K )`
lecmt.l
`|- .<_ = ( le ` K )`
lecmt.c
`|- C = ( cm ` K )`
Assertion lecmtN
`|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> X C Y ) )`

### Proof

Step Hyp Ref Expression
1 lecmt.b
` |-  B = ( Base ` K )`
2 lecmt.l
` |-  .<_ = ( le ` K )`
3 lecmt.c
` |-  C = ( cm ` K )`
4 omllat
` |-  ( K e. OML -> K e. Lat )`
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )`
6 simp2
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )`
7 omlop
` |-  ( K e. OML -> K e. OP )`
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )`
9 eqid
` |-  ( oc ` K ) = ( oc ` K )`
10 1 9 opoccl
` |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )`
11 8 6 10 syl2anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` X ) e. B )`
12 simp3
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )`
13 eqid
` |-  ( join ` K ) = ( join ` K )`
14 1 13 latjcl
` |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ Y e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) e. B )`
15 5 11 12 14 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) e. B )`
16 eqid
` |-  ( meet ` K ) = ( meet ` K )`
17 1 2 16 latmle1
` |-  ( ( K e. Lat /\ X e. B /\ ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) e. B ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ X )`
18 5 6 15 17 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ X )`
19 1 16 latmcl
` |-  ( ( K e. Lat /\ X e. B /\ ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) e. B ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) e. B )`
20 5 6 15 19 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) e. B )`
21 1 2 lattr
` |-  ( ( K e. Lat /\ ( ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ X /\ X .<_ Y ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ Y ) )`
22 5 20 6 12 21 syl13anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ X /\ X .<_ Y ) -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ Y ) )`
23 18 22 mpand
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ Y ) )`
24 1 2 13 16 9 3 cmtbr4N
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ( meet ` K ) ( ( ( oc ` K ) ` X ) ( join ` K ) Y ) ) .<_ Y ) )`
25 23 24 sylibrd
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> X C Y ) )`