Theorem mdslmd2i

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 (join version). (Contributed by NM, 29-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	mdslmd2i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\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	3 4	chjcli	$$⊢C{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
6	5 2 1	chlej1i	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to \left(C{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}A\subseteq B{\vee }_{\mathscr{H}}A$$
7	3 4 1	chjjdiri	$$⊢\left(C{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)$$
8	2 1	chjcomi	$$⊢B{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}B$$
9	6 7 8	3sstr3g	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B$$
10	9	adantl	$$⊢\left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B$$
11	1 3	chub2i	$$⊢A\subseteq C{\vee }_{\mathscr{H}}A$$
12	1 4	chub2i	$$⊢A\subseteq D{\vee }_{\mathscr{H}}A$$
13	11 12	ssini	$$⊢A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
14	10 13	jctil	$$⊢\left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\wedge \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B\right)$$
15	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
16	4 1	chjcli	$$⊢D{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
17	1 2 15 16	mdslmd1i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\wedge \left(C{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\leftrightarrow \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right){𝑀}_{\mathscr{H}}\left(\left(D{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
18	14 17	sylan2	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\leftrightarrow \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right){𝑀}_{\mathscr{H}}\left(\left(D{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
19		id	$$⊢A{𝑀}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B$$
20		inss1	$$⊢C\cap D\subseteq C$$
21		sstr	$$⊢\left(A\cap B\subseteq C\cap D\wedge C\cap D\subseteq C\right)\to A\cap B\subseteq C$$
22	20 21	mpan2	$$⊢A\cap B\subseteq C\cap D\to A\cap B\subseteq C$$
23	3 4	chub1i	$$⊢C\subseteq C{\vee }_{\mathscr{H}}D$$
24		sstr	$$⊢\left(C\subseteq C{\vee }_{\mathscr{H}}D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to C\subseteq B$$
25	23 24	mpan	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to C\subseteq B$$
26	1 2 3	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)$$
27		mdsl3	$$⊢\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\cap B\subseteq C\wedge C\subseteq B\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
28	26 27	mpan	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\wedge C\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
29	19 22 25 28	syl3an	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
30		inss2	$$⊢C\cap D\subseteq D$$
31		sstr	$$⊢\left(A\cap B\subseteq C\cap D\wedge C\cap D\subseteq D\right)\to A\cap B\subseteq D$$
32	30 31	mpan2	$$⊢A\cap B\subseteq C\cap D\to A\cap B\subseteq D$$
33	4 3	chub2i	$$⊢D\subseteq C{\vee }_{\mathscr{H}}D$$
34		sstr	$$⊢\left(D\subseteq C{\vee }_{\mathscr{H}}D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to D\subseteq B$$
35	33 34	mpan	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to D\subseteq B$$
36	1 2 4	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)$$
37		mdsl3	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
38	36 37	mpan	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq D\wedge D\subseteq B\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
39	19 32 35 38	syl3an	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
40	29 39	breq12d	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right){𝑀}_{\mathscr{H}}\left(\left(D{\vee }_{\mathscr{H}}A\right)\cap B\right)\leftrightarrow C{𝑀}_{\mathscr{H}}D\right)$$
41	40	3expb	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right){𝑀}_{\mathscr{H}}\left(\left(D{\vee }_{\mathscr{H}}A\right)\cap B\right)\leftrightarrow C{𝑀}_{\mathscr{H}}D\right)$$
42	41	adantlr	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\right){𝑀}_{\mathscr{H}}\left(\left(D{\vee }_{\mathscr{H}}A\right)\cap B\right)\leftrightarrow C{𝑀}_{\mathscr{H}}D\right)$$
43	18 42	bitr2d	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\right)\to \left(C{𝑀}_{\mathscr{H}}D\leftrightarrow \left(C{\vee }_{\mathscr{H}}A\right){𝑀}_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}A\right)\right)$$