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	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝐶}_{\mathscr{H}}B\wedge A{𝐶}_{\mathscr{H}}C\right)\right)\to A{𝐶}_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}C\right)$$

Proof

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