Theorem mdexchi

Description: An exchange lemma for modular pairs. Lemma 1.6 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdexch.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdexch.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mdexch.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdexchi	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}B\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap B=A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdexch.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdexch.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdexch.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		chjass	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x=C{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
5	3 1 4	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x=C{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
6	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
7		chjcom	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)=\left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x$$
8	6 7	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)=\left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x$$
9		chjcl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}$$
10	1 9	mpan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}$$
11		chjcom	$$⊢\left(A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C=C{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
12	10 3 11	sylancl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C=C{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
13	5 8 12	3eqtr4d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C$$
14	13	ineq1d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B=\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap B$$
15		inass	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B=\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap B\right)$$
16		incom	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap B=B\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
17	1 2	chjcomi	$$⊢A{\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}A$$
18	17	ineq2i	$$⊢B\cap \left(A{\vee }_{\mathscr{H}}B\right)=B\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
19	2 1	chabs2i	$$⊢B\cap \left(B{\vee }_{\mathscr{H}}A\right)=B$$
20	18 19	eqtri	$$⊢B\cap \left(A{\vee }_{\mathscr{H}}B\right)=B$$
21	16 20	eqtri	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap B=B$$
22	21	ineq2i	$$⊢\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap B\right)=\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap B$$
23	15 22	eqtri	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B=\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap B$$
24	14 23	eqtr4di	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B=\left(\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B$$
25	24	ad2antrr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B=\left(\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B$$
26		chlej2	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\subseteq B\right)\to A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B$$
27	26	ex	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\right)$$
28	2 1 27	mp3an23	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\right)$$
29	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
30		mdi	$$⊢\left(\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
31	30	exp32	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
32	3 29 31	mp3an12	$$⊢A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
33	10 32	syl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
34	33	com23	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{\vee }_{\mathscr{H}}x\subseteq A{\vee }_{\mathscr{H}}B\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
35	28 34	syld	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
36	35	imp31	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
37	36	adantrr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
38	3 29	chincli	$$⊢C\cap \left(A{\vee }_{\mathscr{H}}B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
39		chlej2	$$⊢\left(\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A$$
40	39	ex	$$⊢\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A\right)$$
41	38 1 40	mp3an12	$$⊢A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\to \left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A\right)$$
42	10 41	syl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A\right)$$
43	42	imp	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A$$
44		chjcom	$$⊢\left(A{\vee }_{\mathscr{H}}x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
45	10 1 44	sylancl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
46	1	chjidmi	$$⊢A{\vee }_{\mathscr{H}}A=A$$
47	46	oveq1i	$$⊢\left(A{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x=A{\vee }_{\mathscr{H}}x$$
48		chjass	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x=A{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
49	1 1 48	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}x=A{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)$$
50		chjcom	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}A$$
51	1 50	mpan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}A$$
52	47 49 51	3eqtr3a	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}x\right)=x{\vee }_{\mathscr{H}}A$$
53	45 52	eqtrd	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A=x{\vee }_{\mathscr{H}}A$$
54	53	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}A=x{\vee }_{\mathscr{H}}A$$
55	43 54	sseqtrd	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq x{\vee }_{\mathscr{H}}A$$
56	55	ad2ant2rl	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\subseteq x{\vee }_{\mathscr{H}}A$$
57	37 56	eqsstrd	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq x{\vee }_{\mathscr{H}}A$$
58	57	ssrind	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(\left(\left(A{\vee }_{\mathscr{H}}x\right){\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
59	25 58	eqsstrd	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
60	59	adantrl	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\right)\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
61		mdi	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge x\subseteq B\right)\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
62	61	exp32	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}B\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
63	1 2 62	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A{𝑀}_{\mathscr{H}}B\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
64	63	com23	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to \left(A{𝑀}_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
65	64	imp31	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge A{𝑀}_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
66	1 3	chub2i	$$⊢A\subseteq C{\vee }_{\mathscr{H}}A$$
67		ssrin	$$⊢A\subseteq C{\vee }_{\mathscr{H}}A\to A\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B$$
68	66 67	ax-mp	$$⊢A\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B$$
69	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
70	6 2	chincli	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
71		chlej2	$$⊢\left(\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
72	71	ex	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
73	69 70 72	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
74	68 73	mpi	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
75	74	ad2antrr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge A{𝑀}_{\mathscr{H}}B\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
76	65 75	eqsstrd	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge A{𝑀}_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
77	76	adantrr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
78	60 77	sstrd	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\right)\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
79	78	exp31	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to \left(\left(A{𝑀}_{\mathscr{H}}B\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)\right)$$
80	79	com3r	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)\right)$$
81	80	3impb	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)\right)$$
82	81	ralrimiv	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
83		mdbr2	$$⊢\left(C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)\right)$$
84	6 2 83	mp2an	$$⊢\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
85	82 84	sylibr	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}B$$
86	3 1	chjcomi	$$⊢C{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}C$$
87		incom	$$⊢B\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(A{\vee }_{\mathscr{H}}B\right)\cap B$$
88	18 87 19	3eqtr3ri	$$⊢B=\left(A{\vee }_{\mathscr{H}}B\right)\cap B$$
89	86 88	ineq12i	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap B=\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap B\right)$$
90		inass	$$⊢\left(\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B=\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap B\right)$$
91	1 2	chub1i	$$⊢A\subseteq A{\vee }_{\mathscr{H}}B$$
92		mdi	$$⊢\left(\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge A\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
93	92	exp32	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A\subseteq A{\vee }_{\mathscr{H}}B\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)$$
94	3 29 1 93	mp3an	$$⊢C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A\subseteq A{\vee }_{\mathscr{H}}B\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
95	91 94	mpi	$$⊢C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
96	1 38	chjcomi	$$⊢A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)=\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right){\vee }_{\mathscr{H}}A$$
97	38 1	chlejb1i	$$⊢C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\leftrightarrow \left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right){\vee }_{\mathscr{H}}A=A$$
98	97	biimpi	$$⊢C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\to \left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right){\vee }_{\mathscr{H}}A=A$$
99	96 98	syl5eq	$$⊢C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\to A{\vee }_{\mathscr{H}}\left(C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)=A$$
100	95 99	sylan9eq	$$⊢\left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=A$$
101	100	ineq1d	$$⊢\left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\cap B=A\cap B$$
102	90 101	eqtr3id	$$⊢\left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap B\right)=A\cap B$$
103	89 102	syl5eq	$$⊢\left(C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=A\cap B$$
104	103	3adant1	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=A\cap B$$
105	85 104	jca	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge C{𝑀}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\wedge C\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}B\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap B=A\cap B\right)$$