Theorem mdslmd1i

Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2 (meet version). (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdslmd1i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdslmd.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdslmd.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mdslmd.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5		ssin	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\leftrightarrow A\subseteq C\cap D$$
6	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
7	3 4 6	chlubi	$$⊢\left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B$$
8	5 7	anbi12i	$$⊢\left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)$$
9		chjcl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
10	1 9	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
11		sseq1	$$⊢y=x{\vee }_{\mathscr{H}}A\to \left(y\subseteq D\leftrightarrow x{\vee }_{\mathscr{H}}A\subseteq D\right)$$
12		oveq1	$$⊢y=x{\vee }_{\mathscr{H}}A\to y{\vee }_{\mathscr{H}}C=\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C$$
13	12	ineq1d	$$⊢y=x{\vee }_{\mathscr{H}}A\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D=\left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D$$
14		oveq1	$$⊢y=x{\vee }_{\mathscr{H}}A\to y{\vee }_{\mathscr{H}}\left(C\cap D\right)=\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)$$
15	13 14	sseq12d	$$⊢y=x{\vee }_{\mathscr{H}}A\to \left(\left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\leftrightarrow \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)$$
16	11 15	imbi12d	$$⊢y=x{\vee }_{\mathscr{H}}A\to \left(\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
17	16	rspcv	$$⊢x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
18	10 17	syl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
19	18	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
20	1 2 3 4	mdslmd1lem3	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
21	19 20	syld	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
22	21	ex	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)$$
23	22	com3l	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)$$
24	23	ralrimdv	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
25		mdbr2	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
26	3 4 25	mp2an	$$⊢C{𝑀}_{\mathscr{H}}D\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\to \left(y{\vee }_{\mathscr{H}}C\right)\cap D\subseteq y{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)$$
27	3 2	chincli	$$⊢C\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
28	4 2	chincli	$$⊢D\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
29	27 28	mdsl2i	$$⊢\left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)$$
30	24 26 29	3imtr4g	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\to \left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\right)$$
31		chincl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
32	2 31	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
33		sseq1	$$⊢y=x\cap B\to \left(y\subseteq D\cap B\leftrightarrow x\cap B\subseteq D\cap B\right)$$
34		oveq1	$$⊢y=x\cap B\to y{\vee }_{\mathscr{H}}\left(C\cap B\right)=\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
35	34	ineq1d	$$⊢y=x\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)=\left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)$$
36		oveq1	$$⊢y=x\cap B\to y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)=\left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)$$
37	35 36	sseq12d	$$⊢y=x\cap B\to \left(\left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\leftrightarrow \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)$$
38	33 37	imbi12d	$$⊢y=x\cap B\to \left(\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\leftrightarrow \left(x\cap B\subseteq D\cap B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
39	38	rspcv	$$⊢x\cap B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(x\cap B\subseteq D\cap B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
40	32 39	syl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(x\cap B\subseteq D\cap B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
41	40	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(x\cap B\subseteq D\cap B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
42	1 2 3 4	mdslmd1lem4	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\left(x\cap B\subseteq D\cap B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
43	41 42	syld	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
44	43	ex	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)\right)$$
45	44	com3l	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)\right)$$
46	45	ralrimdv	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
47		mdbr2	$$⊢\left(C\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\cap B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
48	27 28 47	mp2an	$$⊢\left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq D\cap B\to \left(y{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq y{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)$$
49	3 4	mdsl2i	$$⊢C{𝑀}_{\mathscr{H}}D\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(C\cap D\subseteq x\wedge x\subseteq D\right)\to \left(x{\vee }_{\mathscr{H}}C\right)\cap D\subseteq x{\vee }_{\mathscr{H}}\left(C\cap D\right)\right)$$
50	46 48 49	3imtr4g	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\to C{𝑀}_{\mathscr{H}}D\right)$$
51	30 50	impbid	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\right)$$
52	8 51	sylan2br	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \left(C\cap B\right){𝑀}_{\mathscr{H}}\left(D\cap B\right)\right)$$