Metamath Proof Explorer


Theorem cm2j

Description: A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of Beran p. 49. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cm2j A C B C C C A 𝐶 B A 𝐶 C A 𝐶 B C

Proof

Step Hyp Ref Expression
1 cmcm A C B C A 𝐶 B B 𝐶 A
2 cmbr B C A C B 𝐶 A B = B A B A
3 2 ancoms A C B C B 𝐶 A B = B A B A
4 1 3 bitrd A C B C A 𝐶 B B = B A B A
5 4 biimpa A C B C A 𝐶 B B = B A B A
6 incom B A = A B
7 incom B A = A B
8 6 7 oveq12i B A B A = A B A B
9 5 8 eqtrdi A C B C A 𝐶 B B = A B A B
10 9 3adantl3 A C B C C C A 𝐶 B B = A B A B
11 10 adantrr A C B C C C A 𝐶 B A 𝐶 C B = A B A B
12 cmcm A C C C A 𝐶 C C 𝐶 A
13 cmbr C C A C C 𝐶 A C = C A C A
14 13 ancoms A C C C C 𝐶 A C = C A C A
15 12 14 bitrd A C C C A 𝐶 C C = C A C A
16 15 biimpa A C C C A 𝐶 C C = C A C A
17 incom C A = A C
18 incom C A = A C
19 17 18 oveq12i C A C A = A C A C
20 16 19 eqtrdi A C C C A 𝐶 C C = A C A C
21 20 3adantl2 A C B C C C A 𝐶 C C = A C A C
22 21 adantrl A C B C C C A 𝐶 B A 𝐶 C C = A C A C
23 11 22 oveq12d A C B C C C A 𝐶 B A 𝐶 C B C = A B A B A C A C
24 chincl A C B C A B C
25 choccl A C A C
26 chincl A C B C A B C
27 25 26 sylan A C B C A B C
28 24 27 jca A C B C A B C A B C
29 chincl A C C C A C C
30 chincl A C C C A C C
31 25 30 sylan A C C C A C C
32 29 31 jca A C C C A C C A C C
33 chj4 A B C A B C A C C A C C A B A B A C A C = A B A C A B A C
34 28 32 33 syl2an A C B C A C C C A B A B A C A C = A B A C A B A C
35 34 3impdi A C B C C C A B A B A C A C = A B A C A B A C
36 35 adantr A C B C C C A 𝐶 B A 𝐶 C A B A B A C A C = A B A C A B A C
37 fh1 A C B C C C A 𝐶 B A 𝐶 C A B C = A B A C
38 incom A B C = B C A
39 37 38 eqtr3di A C B C C C A 𝐶 B A 𝐶 C A B A C = B C A
40 25 3anim1i A C B C C C A C B C C C
41 40 adantr A C B C C C A 𝐶 B A 𝐶 C A C B C C C
42 cmcm3 A C B C A 𝐶 B A 𝐶 B
43 42 3adant3 A C B C C C A 𝐶 B A 𝐶 B
44 cmcm3 A C C C A 𝐶 C A 𝐶 C
45 44 3adant2 A C B C C C A 𝐶 C A 𝐶 C
46 43 45 anbi12d A C B C C C A 𝐶 B A 𝐶 C A 𝐶 B A 𝐶 C
47 46 biimpa A C B C C C A 𝐶 B A 𝐶 C A 𝐶 B A 𝐶 C
48 fh1 A C B C C C A 𝐶 B A 𝐶 C A B C = A B A C
49 41 47 48 syl2anc A C B C C C A 𝐶 B A 𝐶 C A B C = A B A C
50 incom A B C = B C A
51 49 50 eqtr3di A C B C C C A 𝐶 B A 𝐶 C A B A C = B C A
52 39 51 oveq12d A C B C C C A 𝐶 B A 𝐶 C A B A C A B A C = B C A B C A
53 23 36 52 3eqtrd A C B C C C A 𝐶 B A 𝐶 C B C = B C A B C A
54 53 ex A C B C C C A 𝐶 B A 𝐶 C B C = B C A B C A
55 chjcl B C C C B C C
56 cmcm A C B C C A 𝐶 B C B C 𝐶 A
57 cmbr B C C A C B C 𝐶 A B C = B C A B C A
58 57 ancoms A C B C C B C 𝐶 A B C = B C A B C A
59 56 58 bitrd A C B C C A 𝐶 B C B C = B C A B C A
60 55 59 sylan2 A C B C C C A 𝐶 B C B C = B C A B C A
61 60 3impb A C B C C C A 𝐶 B C B C = B C A B C A
62 54 61 sylibrd A C B C C C A 𝐶 B A 𝐶 C A 𝐶 B C
63 62 imp A C B C C C A 𝐶 B A 𝐶 C A 𝐶 B C