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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`