Theorem mdslj2i

Description: Meet preservation of the reverse 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	mdslj2i	$$⊢\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\cap D\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\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	3 4 1	lejdiri	$$⊢\left(C\cap D\right){\vee }_{\mathscr{H}}A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
6	5	a1i	$$⊢\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\cap D\right){\vee }_{\mathscr{H}}A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
7		ssin	$$⊢\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\leftrightarrow A\cap B\subseteq C\cap D$$
8	7	bicomi	$$⊢A\cap B\subseteq C\cap D\leftrightarrow \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)$$
9	3 4 2	chlubi	$$⊢\left(C\subseteq B\wedge D\subseteq B\right)\leftrightarrow C{\vee }_{\mathscr{H}}D\subseteq B$$
10	9	bicomi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\leftrightarrow \left(C\subseteq B\wedge D\subseteq B\right)$$
11	8 10	anbi12i	$$⊢\left(A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\leftrightarrow \left(\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)$$
12		simpr	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to B{𝑀}_{\mathscr{H}}^{*}A$$
13	1 3	chub2i	$$⊢A\subseteq C{\vee }_{\mathscr{H}}A$$
14	1 4	chub2i	$$⊢A\subseteq D{\vee }_{\mathscr{H}}A$$
15	13 14	ssini	$$⊢A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
16	15	a1i	$$⊢\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\to A\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
17	3 2 1	chlej1i	$$⊢C\subseteq B\to C{\vee }_{\mathscr{H}}A\subseteq B{\vee }_{\mathscr{H}}A$$
18	2 1	chjcomi	$$⊢B{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}B$$
19	17 18	sseqtrdi	$$⊢C\subseteq B\to C{\vee }_{\mathscr{H}}A\subseteq A{\vee }_{\mathscr{H}}B$$
20		ssinss1	$$⊢C{\vee }_{\mathscr{H}}A\subseteq A{\vee }_{\mathscr{H}}B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B$$
21	19 20	syl	$$⊢C\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B$$
22	21	adantr	$$⊢\left(C\subseteq B\wedge D\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B$$
23	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
24	4 1	chjcli	$$⊢D{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
25	23 24	chincli	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
26	1 2 25	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}\right)$$
27		dmdsl3	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge 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)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
28	26 27	mpan	$$⊢\left(B{𝑀}_{\mathscr{H}}^{*}A\wedge 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)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
29	12 16 22 28	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$
30		inss1	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq C{\vee }_{\mathscr{H}}A$$
31		ssrin	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq C{\vee }_{\mathscr{H}}A\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B$$
32	30 31	ax-mp	$$⊢\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap B$$
33		simpl	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to A{𝑀}_{\mathscr{H}}B$$
34		simpl	$$⊢\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\to A\cap B\subseteq C$$
35		simpl	$$⊢\left(C\subseteq B\wedge D\subseteq B\right)\to C\subseteq B$$
36	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)$$
37		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$$
38	36 37	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$$
39	33 34 35 38	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
40	32 39	sseqtrid	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq C$$
41		inss2	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq D{\vee }_{\mathscr{H}}A$$
42		ssrin	$$⊢\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq D{\vee }_{\mathscr{H}}A\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(D{\vee }_{\mathscr{H}}A\right)\cap B$$
43	41 42	ax-mp	$$⊢\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq \left(D{\vee }_{\mathscr{H}}A\right)\cap B$$
44		simpr	$$⊢\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\to A\cap B\subseteq D$$
45		simpr	$$⊢\left(C\subseteq B\wedge D\subseteq B\right)\to D\subseteq B$$
46	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)$$
47		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$$
48	46 47	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$$
49	33 44 45 48	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
50	43 49	sseqtrid	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq D$$
51	40 50	ssind	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq C\cap D$$
52	25 2	chincli	$$⊢\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
53	3 4	chincli	$$⊢C\cap D\in {\mathbf{C}}_{\mathscr{H}}$$
54	52 53 1	chlej1i	$$⊢\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\subseteq C\cap D\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(C\cap D\right){\vee }_{\mathscr{H}}A$$
55	51 54	syl	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(\left(\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\right)\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(C\cap D\right){\vee }_{\mathscr{H}}A$$
56	29 55	eqsstrrd	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq \left(C\cap D\right){\vee }_{\mathscr{H}}A$$
57	56	3expb	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\wedge \left(C\subseteq B\wedge D\subseteq B\right)\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq \left(C\cap D\right){\vee }_{\mathscr{H}}A$$
58	11 57	sylan2b	$$⊢\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{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)\subseteq \left(C\cap D\right){\vee }_{\mathscr{H}}A$$
59	6 58	eqssd	$$⊢\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\cap D\right){\vee }_{\mathscr{H}}A=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(D{\vee }_{\mathscr{H}}A\right)$$