# Metamath Proof Explorer

## Theorem cmtbr3N

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. ( cmbr3 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cmtbr2.b
` |-  B = ( Base ` K )`
2 cmtbr2.j
` |-  .\/ = ( join ` K )`
3 cmtbr2.m
` |-  ./\ = ( meet ` K )`
4 cmtbr2.o
` |-  ._|_ = ( oc ` K )`
5 cmtbr2.c
` |-  C = ( cm ` K )`
6 1 5 cmtcomN
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y C X ) )`
7 1 2 3 4 5 cmtbr2N
` |-  ( ( K e. OML /\ Y e. B /\ X e. B ) -> ( Y C X <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
8 7 3com23
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y C X <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
9 6 8 bitrd
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
10 oveq2
` |-  ( Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) -> ( X ./\ Y ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ Y ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
12 omlol
` |-  ( K e. OML -> K e. OL )`
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OL )`
14 simp2
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )`
15 omllat
` |-  ( K e. OML -> K e. Lat )`
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )`
17 simp3
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )`
18 1 2 latjcl
` |-  ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .\/ X ) e. B )`
19 16 17 14 18 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ X ) e. B )`
20 omlop
` |-  ( K e. OML -> K e. OP )`
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )`
22 1 4 opoccl
` |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )`
23 21 14 22 syl2anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )`
24 1 2 latjcl
` |-  ( ( K e. Lat /\ Y e. B /\ ( ._|_ ` X ) e. B ) -> ( Y .\/ ( ._|_ ` X ) ) e. B )`
25 16 17 23 24 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ ( ._|_ ` X ) ) e. B )`
26 1 3 latmassOLD
` |-  ( ( K e. OL /\ ( X e. B /\ ( Y .\/ X ) e. B /\ ( Y .\/ ( ._|_ ` X ) ) e. B ) ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
27 13 14 19 25 26 syl13anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) )`
28 1 2 latjcom
` |-  ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .\/ X ) = ( X .\/ Y ) )`
29 16 17 14 28 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ X ) = ( X .\/ Y ) )`
30 29 oveq2d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( Y .\/ X ) ) = ( X ./\ ( X .\/ Y ) ) )`
31 1 2 3 latabs2
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ ( X .\/ Y ) ) = X )`
32 15 31 syl3an1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( X .\/ Y ) ) = X )`
33 30 32 eqtrd
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( Y .\/ X ) ) = X )`
34 1 2 latjcom
` |-  ( ( K e. Lat /\ Y e. B /\ ( ._|_ ` X ) e. B ) -> ( Y .\/ ( ._|_ ` X ) ) = ( ( ._|_ ` X ) .\/ Y ) )`
35 16 17 23 34 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y .\/ ( ._|_ ` X ) ) = ( ( ._|_ ` X ) .\/ Y ) )`
36 33 35 oveq12d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( Y .\/ X ) ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )`
37 27 36 eqtr3d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )`
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )`
39 11 38 eqtr2d
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) )`
40 39 ex
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y = ( ( Y .\/ X ) ./\ ( Y .\/ ( ._|_ ` X ) ) ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )`
41 9 40 sylbid
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )`
42 simp1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )`
43 1 4 opoccl
` |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )`
44 21 17 43 syl2anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )`
45 1 3 latmcl
` |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X ./\ ( ._|_ ` Y ) ) e. B )`
46 16 14 44 45 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` Y ) ) e. B )`
47 42 46 14 3jca
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( K e. OML /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ X e. B ) )`
48 eqid
` |-  ( le ` K ) = ( le ` K )`
49 1 48 3 latmle1
` |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X )`
50 16 14 44 49 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X )`
51 1 48 2 3 4 omllaw2N
` |-  ( ( K e. OML /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ X e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) ( le ` K ) X -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = X ) )`
52 47 50 51 sylc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = X )`
53 1 4 opoccl
` |-  ( ( K e. OP /\ ( X ./\ ( ._|_ ` Y ) ) e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B )`
54 21 46 53 syl2anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B )`
55 1 3 latmcl
` |-  ( ( K e. Lat /\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B /\ X e. B ) -> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B )`
56 16 54 14 55 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B )`
57 1 2 latjcom
` |-  ( ( K e. Lat /\ ( X ./\ ( ._|_ ` Y ) ) e. B /\ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
58 16 46 56 57 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) ) = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
59 52 58 eqtr3d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> X = ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
61 1 2 3 4 oldmm3N
` |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) .\/ Y ) )`
62 12 61 syl3an1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) .\/ Y ) )`
63 62 oveq2d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) )`
64 1 3 latmcom
` |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )`
65 16 14 54 64 syl3anc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )`
66 63 65 eqtr3d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) )`
67 66 eqeq1d
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) <-> ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) = ( X ./\ Y ) ) )`
68 oveq1
` |-  ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) = ( X ./\ Y ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
69 67 68 syl6bi
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )`
70 69 imp
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> ( ( ( ._|_ ` ( X ./\ ( ._|_ ` Y ) ) ) ./\ X ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
71 60 70 eqtrd
` |-  ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) -> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )`
72 71 ex
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )`
73 1 2 3 4 5 cmtvalN
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )`
74 72 73 sylibrd
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) -> X C Y ) )`
75 41 74 impbid
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ./\ ( ( ._|_ ` X ) .\/ Y ) ) = ( X ./\ Y ) ) )`