Theorem mdslj1i

Description: Join 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	mdslj1i	$$⊢\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{\vee }_{\mathscr{H}}D\right)\cap B=\left(C\cap B\right){\vee }_{\mathscr{H}}\left(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		ssin	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\leftrightarrow A\subseteq C\cap D$$
6	5	bicomi	$$⊢A\subseteq C\cap D\leftrightarrow \left(A\subseteq C\wedge A\subseteq D\right)$$
7	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
8	3 4 7	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$$
9	8	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)$$
10	6 9	anbi12i	$$⊢\left(A\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \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)$$
11		simpr	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to B{𝑀}_{\mathscr{H}}^{*}A$$
12		simpl	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\to A\subseteq C$$
13		simpl	$$⊢\left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\to C\subseteq A{\vee }_{\mathscr{H}}B$$
14	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)$$
15		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$$
16	14 15	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$$
17	11 12 13 16	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$
18	3 2	chincli	$$⊢C\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
19	4 2	chincli	$$⊢D\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
20	18 19	chub1i	$$⊢C\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
21	18 19	chjcli	$$⊢\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
22	18 21 1	chlej1i	$$⊢C\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
23	20 22	mp1i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
24	17 23	eqsstrrd	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to C\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
25		simpr	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\to A\subseteq D$$
26		simpr	$$⊢\left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\to D\subseteq A{\vee }_{\mathscr{H}}B$$
27	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)$$
28		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$$
29	27 28	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$$
30	11 25 26 29	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A=D$$
31	19 18	chub2i	$$⊢D\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
32	19 21 1	chlej1i	$$⊢D\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
33	31 32	mp1i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(D\cap B\right){\vee }_{\mathscr{H}}A\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
34	30 33	eqsstrrd	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to D\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
35	24 34	jca	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(C\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\wedge D\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)$$
36	21 1	chjcli	$$⊢\left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
37	3 4 36	chlubi	$$⊢\left(C\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\wedge D\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)\leftrightarrow C{\vee }_{\mathscr{H}}D\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
38	35 37	sylib	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to C{\vee }_{\mathscr{H}}D\subseteq \left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A$$
39	38	ssrind	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(C{\vee }_{\mathscr{H}}D\right)\cap B\subseteq \left(\left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)\cap B$$
40		simpl	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\to A{𝑀}_{\mathscr{H}}B$$
41		ssrin	$$⊢A\subseteq C\to A\cap B\subseteq C\cap B$$
42	41 20	sstrdi	$$⊢A\subseteq C\to A\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
43	42	adantr	$$⊢\left(A\subseteq C\wedge A\subseteq D\right)\to A\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
44		inss2	$$⊢C\cap B\subseteq B$$
45		inss2	$$⊢D\cap B\subseteq B$$
46	18 19 2	chlubi	$$⊢\left(C\cap B\subseteq B\wedge D\cap B\subseteq B\right)\leftrightarrow \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B$$
47	46	bicomi	$$⊢\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B\leftrightarrow \left(C\cap B\subseteq B\wedge D\cap B\subseteq B\right)$$
48	44 45 47	mpbir2an	$$⊢\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B$$
49	48	a1i	$$⊢\left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B$$
50	1 2 21	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}\right)$$
51		mdsl3	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\wedge \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B\right)\right)\to \left(\left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)\cap B=\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
52	50 51	mpan	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\wedge \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq B\right)\to \left(\left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)\cap B=\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
53	40 43 49 52	syl3an	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(\left(\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\right){\vee }_{\mathscr{H}}A\right)\cap B=\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
54	39 53	sseqtrd	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \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)\to \left(C{\vee }_{\mathscr{H}}D\right)\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
55	54	3expb	$$⊢\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{\vee }_{\mathscr{H}}D\right)\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
56	10 55	sylan2b	$$⊢\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{\vee }_{\mathscr{H}}D\right)\cap B\subseteq \left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$
57	3 4 2	lediri	$$⊢\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq \left(C{\vee }_{\mathscr{H}}D\right)\cap B$$
58	57	a1i	$$⊢\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\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)\subseteq \left(C{\vee }_{\mathscr{H}}D\right)\cap B$$
59	56 58	eqssd	$$⊢\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{\vee }_{\mathscr{H}}D\right)\cap B=\left(C\cap B\right){\vee }_{\mathscr{H}}\left(D\cap B\right)$$