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 )
5 4 3ad2ant1 
 |-  ( ( 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 )
8 7 3ad2ant1 
 |-  ( ( 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 ) )