# 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}={\mathrm{Base}}_{{K}}$
cmtbr2.j
cmtbr2.m
cmtbr2.o
cmtbr2.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion cmtbr3N

### Proof

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