Theorem cm2jt 9563

Description: A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of [Beran] p. 49.

Assertion

Ref	Expression
cm2jt	|- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> A C_H (B vH C))

Proof of Theorem cm2jt

Step	Hyp	Ref	Expression
1		cmcmt 9557	. . . . . . . . . . 11 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> B C_H A))
2		cmbrt 9527	. . . . . . . . . . . 12 |- ((B e. CH /\ A e. CH) -> (B C_H A <-> B = ((B i^i A) vH (B i^i (_|_` A)))))
3	2	ancoms 436	. . . . . . . . . . 11 |- ((A e. CH /\ B e. CH) -> (B C_H A <-> B = ((B i^i A) vH (B i^i (_|_` A)))))
4	1, 3	bitrd 528	. . . . . . . . . 10 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> B = ((B i^i A) vH (B i^i (_|_` A)))))
5	4	biimpa 416	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ A C_H B) -> B = ((B i^i A) vH (B i^i (_|_` A))))
6		incom 2208	. . . . . . . . . 10 |- (B i^i A) = (A i^i B)
7		incom 2208	. . . . . . . . . 10 |- (B i^i (_|_` A)) = ((_|_` A) i^i B)
8	6, 7	opreq12i 3973	. . . . . . . . 9 |- ((B i^i A) vH (B i^i (_|_` A))) = ((A i^i B) vH ((_|_` A) i^i B))
9	5, 8	syl6eq 1523	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ A C_H B) -> B = ((A i^i B) vH ((_|_` A) i^i B)))
10	9	3adantl3 805	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ A C_H B) -> B = ((A i^i B) vH ((_|_` A) i^i B)))
11	10	adantrr 395	. . . . . 6 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> B = ((A i^i B) vH ((_|_` A) i^i B)))
12		cmcmt 9557	. . . . . . . . . . 11 |- ((A e. CH /\ C e. CH) -> (A C_H C <-> C C_H A))
13		cmbrt 9527	. . . . . . . . . . . 12 |- ((C e. CH /\ A e. CH) -> (C C_H A <-> C = ((C i^i A) vH (C i^i (_|_` A)))))
14	13	ancoms 436	. . . . . . . . . . 11 |- ((A e. CH /\ C e. CH) -> (C C_H A <-> C = ((C i^i A) vH (C i^i (_|_` A)))))
15	12, 14	bitrd 528	. . . . . . . . . 10 |- ((A e. CH /\ C e. CH) -> (A C_H C <-> C = ((C i^i A) vH (C i^i (_|_` A)))))
16	15	biimpa 416	. . . . . . . . 9 |- (((A e. CH /\ C e. CH) /\ A C_H C) -> C = ((C i^i A) vH (C i^i (_|_` A))))
17		incom 2208	. . . . . . . . . 10 |- (C i^i A) = (A i^i C)
18		incom 2208	. . . . . . . . . 10 |- (C i^i (_|_` A)) = ((_|_` A) i^i C)
19	17, 18	opreq12i 3973	. . . . . . . . 9 |- ((C i^i A) vH (C i^i (_|_` A))) = ((A i^i C) vH ((_|_` A) i^i C))
20	16, 19	syl6eq 1523	. . . . . . . 8 |- (((A e. CH /\ C e. CH) /\ A C_H C) -> C = ((A i^i C) vH ((_|_` A) i^i C)))
21	20	3adantl2 804	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ A C_H C) -> C = ((A i^i C) vH ((_|_` A) i^i C)))
22	21	adantrl 394	. . . . . 6 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> C = ((A i^i C) vH ((_|_` A) i^i C)))
23	11, 22	opreq12d 3978	. . . . 5 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (B vH C) = (((A i^i B) vH ((_|_` A) i^i B)) vH ((A i^i C) vH ((_|_` A) i^i C))))
24		chj4t 9458	. . . . . . . 8 |- ((((A i^i B) e. CH /\ ((_|_` A) i^i B) e. CH) /\ ((A i^i C) e. CH /\ ((_|_` A) i^i C) e. CH)) -> (((A i^i B) vH ((_|_` A) i^i B)) vH ((A i^i C) vH ((_|_` A) i^i C))) = (((A i^i B) vH (A i^i C)) vH (((_|_` A) i^i B) vH ((_|_` A) i^i C))))
25		chinclt 9422	. . . . . . . . 9 |- ((A e. CH /\ B e. CH) -> (A i^i B) e. CH)
26		chinclt 9422	. . . . . . . . . 10 |- (((_|_` A) e. CH /\ B e. CH) -> ((_|_` A) i^i B) e. CH)
27		chocclt 9184	. . . . . . . . . 10 |- (A e. CH -> (_|_` A) e. CH)
28	26, 27	sylan 448	. . . . . . . . 9 |- ((A e. CH /\ B e. CH) -> ((_|_` A) i^i B) e. CH)
29	25, 28	jca 288	. . . . . . . 8 |- ((A e. CH /\ B e. CH) -> ((A i^i B) e. CH /\ ((_|_` A) i^i B) e. CH))
30		chinclt 9422	. . . . . . . . 9 |- ((A e. CH /\ C e. CH) -> (A i^i C) e. CH)
31		chinclt 9422	. . . . . . . . . 10 |- (((_|_` A) e. CH /\ C e. CH) -> ((_|_` A) i^i C) e. CH)
32	31, 27	sylan 448	. . . . . . . . 9 |- ((A e. CH /\ C e. CH) -> ((_|_` A) i^i C) e. CH)
33	30, 32	jca 288	. . . . . . . 8 |- ((A e. CH /\ C e. CH) -> ((A i^i C) e. CH /\ ((_|_` A) i^i C) e. CH))
34	24, 29, 33	syl2an 454	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (((A i^i B) vH ((_|_` A) i^i B)) vH ((A i^i C) vH ((_|_` A) i^i C))) = (((A i^i B) vH (A i^i C)) vH (((_|_` A) i^i B) vH ((_|_` A) i^i C))))
35	34	3impdi 880	. . . . . 6 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (((A i^i B) vH ((_|_` A) i^i B)) vH ((A i^i C) vH ((_|_` A) i^i C))) = (((A i^i B) vH (A i^i C)) vH (((_|_` A) i^i B) vH ((_|_` A) i^i C))))
36	35	adantr 389	. . . . 5 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (((A i^i B) vH ((_|_` A) i^i B)) vH ((A i^i C) vH ((_|_` A) i^i C))) = (((A i^i B) vH (A i^i C)) vH (((_|_` A) i^i B) vH ((_|_` A) i^i C))))
37		fh1t 9561	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (A i^i (B vH C)) = ((A i^i B) vH (A i^i C)))
38		incom 2208	. . . . . . 7 |- (A i^i (B vH C)) = ((B vH C) i^i A)
39	37, 38	syl5reqr 1522	. . . . . 6 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((A i^i B) vH (A i^i C)) = ((B vH C) i^i A))
40		fh1t 9561	. . . . . . . 8 |- ((((_|_` A) e. CH /\ B e. CH /\ C e. CH) /\ ((_|_` A) C_H B /\ (_|_` A) C_H C)) -> ((_|_` A) i^i (B vH C)) = (((_|_` A) i^i B) vH ((_|_` A) i^i C)))
41		id 59	. . . . . . . . . 10 |- (B e. CH -> B e. CH)
42		id 59	. . . . . . . . . 10 |- (C e. CH -> C e. CH)
43	27, 41, 42	3anim123i 821	. . . . . . . . 9 |- ((A e. CH /\ B e. CH /\ C e. CH) -> ((_|_` A) e. CH /\ B e. CH /\ C e. CH))
44	43	adantr 389	. . . . . . . 8 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((_|_` A) e. CH /\ B e. CH /\ C e. CH))
45		cmcm3t 9558	. . . . . . . . . . 11 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> (_|_` A) C_H B))
46	45	3adant3 799	. . . . . . . . . 10 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (A C_H B <-> (_|_` A) C_H B))
47		cmcm3t 9558	. . . . . . . . . . 11 |- ((A e. CH /\ C e. CH) -> (A C_H C <-> (_|_` A) C_H C))
48	47	3adant2 798	. . . . . . . . . 10 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (A C_H C <-> (_|_` A) C_H C))
49	46, 48	anbi12d 628	. . . . . . . . 9 |- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A C_H B /\ A C_H C) <-> ((_|_` A) C_H B /\ (_|_` A) C_H C)))
50	49	biimpa 416	. . . . . . . 8 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((_|_` A) C_H B /\ (_|_` A) C_H C))
51	40, 44, 50	sylanc 471	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((_|_