Theorem mdslle1i

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

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

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdslle1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdslle1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mdslle1.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5		ssrin	$$⊢C\subseteq D\to C\cap B\subseteq D\cap B$$
6	3 2	chincli	$$⊢C\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
7	4 2	chincli	$$⊢D\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
8	6 7 1	chlej1i	$$⊢C\cap B\subseteq D\cap B\to \left(C\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(D\cap B\right){\vee }_{\mathscr{H}}A$$
9		id	$$⊢B{𝑀}_{\mathscr{H}}^{*}A\to B{𝑀}_{\mathscr{H}}^{*}A$$
10		ssin	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\leftrightarrow A\subseteq C\cap D$$
11	10	bicomi	$$⊢A\subseteq C\cap D\leftrightarrow \left(A\subseteq C\wedge A\subseteq D\right)$$
12	11	simplbi	$$⊢A\subseteq C\cap D\to A\subseteq C$$
13	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
14	3 4 13	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$$
15	14	bicomi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)$$
16	15	simplbi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\to C\subseteq A{\vee }_{\mathscr{H}}B$$
17	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)$$
18		dmdsl3	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$
19	17 18	mpan	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$
20	9 12 16 19	syl3an	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$
21	11	simprbi	$$⊢A\subseteq C\cap D\to A\subseteq D$$
22	15	simprbi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\to D\subseteq A{\vee }_{\mathscr{H}}B$$
23	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)$$
24		dmdsl3	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq D\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A=D$$
25	23 24	mpan	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq D\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A=D$$
26	9 21 22 25	syl3an	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A=D$$
27	20 26	sseq12d	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(\left(C\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(D\cap B\right){\vee }_{\mathscr{H}}A\leftrightarrow C\subseteq D\right)$$
28	8 27	imbitrid	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(C\cap B\subseteq D\cap B\to C\subseteq D\right)$$
29	5 28	impbid2	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(C\subseteq D\leftrightarrow C\cap B\subseteq D\cap B\right)$$