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 = Base K
cmtbr2.j ˙ = join K
cmtbr2.m ˙ = meet K
cmtbr2.o ˙ = oc K
cmtbr2.c C = cm K
Assertion cmtbr2N K OML X B Y 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 4 5 cmt4N K OML X B Y B X C Y ˙ X C ˙ Y
7 simp1 K OML X B Y B K OML
8 omlop K OML K OP
9 8 3ad2ant1 K OML X B Y B K OP
10 simp2 K OML X B Y B X B
11 1 4 opoccl K OP X B ˙ X B
12 9 10 11 syl2anc K OML X B Y B ˙ X B
13 simp3 K OML X B Y B Y B
14 1 4 opoccl K OP Y B ˙ Y B
15 9 13 14 syl2anc K OML X B Y B ˙ Y B
16 1 2 3 4 5 cmtvalN K OML ˙ X B ˙ Y B ˙ X C ˙ Y ˙ X = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y
17 7 12 15 16 syl3anc K OML X B Y B ˙ X C ˙ Y ˙ X = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y
18 eqcom X = X ˙ Y ˙ X ˙ ˙ Y X ˙ Y ˙ X ˙ ˙ Y = X
19 18 a1i K OML X B Y B X = X ˙ Y ˙ X ˙ ˙ Y X ˙ Y ˙ X ˙ ˙ Y = X
20 omllat K OML K Lat
21 20 3ad2ant1 K OML X B Y B K Lat
22 1 2 latjcl K Lat X B Y B X ˙ Y B
23 20 22 syl3an1 K OML X B Y B X ˙ Y B
24 1 2 latjcl K Lat X B ˙ Y B X ˙ ˙ Y B
25 21 10 15 24 syl3anc K OML X B Y B X ˙ ˙ Y B
26 1 3 latmcl K Lat X ˙ Y B X ˙ ˙ Y B X ˙ Y ˙ X ˙ ˙ Y B
27 21 23 25 26 syl3anc K OML X B Y B X ˙ Y ˙ X ˙ ˙ Y B
28 1 4 opcon3b K OP X ˙ Y ˙ X ˙ ˙ Y B X B X ˙ Y ˙ X ˙ ˙ Y = X ˙ X = ˙ X ˙ Y ˙ X ˙ ˙ Y
29 9 27 10 28 syl3anc K OML X B Y B X ˙ Y ˙ X ˙ ˙ Y = X ˙ X = ˙ X ˙ Y ˙ X ˙ ˙ Y
30 omlol K OML K OL
31 30 3ad2ant1 K OML X B Y B K OL
32 1 2 3 4 oldmm1 K OL X ˙ Y B X ˙ ˙ Y B ˙ X ˙ Y ˙ X ˙ ˙ Y = ˙ X ˙ Y ˙ ˙ X ˙ ˙ Y
33 31 23 25 32 syl3anc K OML X B Y B ˙ X ˙ Y ˙ X ˙ ˙ Y = ˙ X ˙ Y ˙ ˙ X ˙ ˙ Y
34 1 2 3 4 oldmj1 K OL X B Y B ˙ X ˙ Y = ˙ X ˙ ˙ Y
35 30 34 syl3an1 K OML X B Y B ˙ X ˙ Y = ˙ X ˙ ˙ Y
36 1 2 3 4 oldmj1 K OL X B ˙ Y B ˙ X ˙ ˙ Y = ˙ X ˙ ˙ ˙ Y
37 31 10 15 36 syl3anc K OML X B Y B ˙ X ˙ ˙ Y = ˙ X ˙ ˙ ˙ Y
38 35 37 oveq12d K OML X B Y B ˙ X ˙ Y ˙ ˙ X ˙ ˙ Y = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y
39 33 38 eqtrd K OML X B Y B ˙ X ˙ Y ˙ X ˙ ˙ Y = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y
40 39 eqeq2d K OML X B Y B ˙ X = ˙ X ˙ Y ˙ X ˙ ˙ Y ˙ X = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y
41 19 29 40 3bitrrd K OML X B Y B ˙ X = ˙ X ˙ ˙ Y ˙ ˙ X ˙ ˙ ˙ Y X = X ˙ Y ˙ X ˙ ˙ Y
42 6 17 41 3bitrd K OML X B Y B X C Y X = X ˙ Y ˙ X ˙ ˙ Y