# Metamath Proof Explorer

## Theorem cmtbr2N

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. ( cmbr2i 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 cmtbr2N

### 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 4 5 cmt4N
7 simp1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OML}$
8 omlop ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OP}$
9 8 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OP}$
10 simp2 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
11 1 4 opoccl
12 9 10 11 syl2anc
13 simp3 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
14 1 4 opoccl
15 9 13 14 syl2anc
16 1 2 3 4 5 cmtvalN
17 7 12 15 16 syl3anc
18 eqcom
19 18 a1i
20 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
21 20 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
22 1 2 latjcl
23 20 22 syl3an1
24 1 2 latjcl
25 21 10 15 24 syl3anc
26 1 3 latmcl
27 21 23 25 26 syl3anc
28 1 4 opcon3b
29 9 27 10 28 syl3anc
30 omlol ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OL}$
31 30 3ad2ant1 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OL}$
32 1 2 3 4 oldmm1
33 31 23 25 32 syl3anc
34 1 2 3 4 oldmj1
35 30 34 syl3an1
36 1 2 3 4 oldmj1
37 31 10 15 36 syl3anc
38 35 37 oveq12d
39 33 38 eqtrd
40 39 eqeq2d
41 19 29 40 3bitrrd
42 6 17 41 3bitrd