Metamath Proof Explorer

Theorem cmtbr4N

Description: Alternate definition for the commutes relation. ( cmbr4i analog.) (Contributed by NM, 10-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtbr4.b 
|- B = ( Base ` K )
cmtbr4.l 
|- .<_ = ( le ` K )
cmtbr4.j 
|- .\/ = ( join ` K )
cmtbr4.m 
|- ./\ = ( meet ` K )
cmtbr4.o 
|- ._|_ = ( oc ` K )
cmtbr4.c 
|- C = ( cm ` K )
Assertion cmtbr4N 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) )

Proof

Step Hyp Ref Expression
1 cmtbr4.b 
 |-  B = ( Base ` K )
2 cmtbr4.l 
 |-  .<_ = ( le ` K )
3 cmtbr4.j 
 |-  .\/ = ( join ` K )
4 cmtbr4.m 
 |-  ./\ = ( meet ` K )
5 cmtbr4.o 
 |-  ._|_ = ( oc ` K )
6 cmtbr4.c 
 |-  C = ( cm ` K )
7 1 3 4 5 6 cmtbr3N 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
8 omllat 
 |-  ( K e. OML -> K e. Lat )
9 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )
10 8 9 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )
11 breq1 
 |-  ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y <-> ( X ./\ Y ) .<_ Y ) )
12 10 11 syl5ibrcom 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) )
13 8 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
14 simp2 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
15 omlop 
 |-  ( K e. OML -> K e. OP )
16 15 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )
17 1 5 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
18 16 14 17 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
19 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
20 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .\/ Y ) e. B )
21 13 18 19 20 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) .\/ Y ) e. B )
22 1 2 4 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ ( ( ._|_ ` X ) .\/ Y ) e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X )
23 13 14 21 22 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X )
24 23 anim1i 
 |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) )
25 24 ex 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) ) )
26 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( ( ._|_ ` X ) .\/ Y ) e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) e. B )
27 13 14 21 26 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) e. B )
28 1 2 4 latlem12 
 |-  ( ( K e. Lat /\ ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) ) )
29 13 27 14 19 28 syl13anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ X /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) ) )
30 25 29 sylibd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) ) )
31 1 2 3 latlej2 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ Y e. B ) -> Y .<_ ( ( ._|_ ` X ) .\/ Y ) )
32 13 18 19 31 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y .<_ ( ( ._|_ ` X ) .\/ Y ) )
33 1 2 4 latmlem2 
 |-  ( ( K e. Lat /\ ( Y e. B /\ ( ( ._|_ ` X ) .\/ Y ) e. B /\ X e. B ) ) -> ( Y .<_ ( ( ._|_ ` X ) .\/ Y ) -> ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) ) )
34 13 19 21 14 33 syl13anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .<_ ( ( ._|_ ` X ) .\/ Y ) -> ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) ) )
35 32 34 mpd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )
36 30 35 jctird 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) ) ) )
37 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
38 8 37 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
39 1 2 latasymb 
 |-  ( ( K e. Lat /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) e. B /\ ( X ./\ Y ) e. B ) -> ( ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) ) <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
40 13 27 38 39 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) ) <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
41 36 40 sylibd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )
42 12 41 impbid 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) )
43 7 42 bitrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) .<_ Y ) )