Theorem mdslmd4i

Description: Modular pair condition that implies the modular pair property in a sublattice. Lemma 1.5.2 of MaedaMaeda p. 2. (Contributed by NM, 24-Dec-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	mdslmd4i	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to C{𝑀}_{\mathscr{H}}D$$

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		simp1	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to A{𝑀}_{\mathscr{H}}B$$
6	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
7		ssmd1	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\wedge A\cap B\subseteq D\right)\to \left(A\cap B\right){𝑀}_{\mathscr{H}}D$$
8	6 4 7	mp3an12	$$⊢A\cap B\subseteq D\to \left(A\cap B\right){𝑀}_{\mathscr{H}}D$$
9	8	adantr	$$⊢\left(A\cap B\subseteq D\wedge D\subseteq B\right)\to \left(A\cap B\right){𝑀}_{\mathscr{H}}D$$
10	9	3ad2ant3	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to \left(A\cap B\right){𝑀}_{\mathscr{H}}D$$
11		sslin	$$⊢D\subseteq B\to A\cap D\subseteq A\cap B$$
12		sstr	$$⊢\left(A\cap D\subseteq A\cap B\wedge A\cap B\subseteq C\right)\to A\cap D\subseteq C$$
13	11 12	sylan	$$⊢\left(D\subseteq B\wedge A\cap B\subseteq C\right)\to A\cap D\subseteq C$$
14	13	ancoms	$$⊢\left(A\cap B\subseteq C\wedge D\subseteq B\right)\to A\cap D\subseteq C$$
15	14	ad2ant2rl	$$⊢\left(\left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to A\cap D\subseteq C$$
16	15	3adant1	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to A\cap D\subseteq C$$
17		simp2r	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to C\subseteq A$$
18	1 2 4 3	mdslmd3i	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\right){𝑀}_{\mathscr{H}}D\right)\wedge \left(A\cap D\subseteq C\wedge C\subseteq A\right)\right)\to C{𝑀}_{\mathscr{H}}\left(B\cap D\right)$$
19	5 10 16 17 18	syl22anc	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to C{𝑀}_{\mathscr{H}}\left(B\cap D\right)$$
20		sseqin2	$$⊢D\subseteq B\leftrightarrow B\cap D=D$$
21	20	biimpi	$$⊢D\subseteq B\to B\cap D=D$$
22	21	adantl	$$⊢\left(A\cap B\subseteq D\wedge D\subseteq B\right)\to B\cap D=D$$
23	22	3ad2ant3	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to B\cap D=D$$
24	19 23	breqtrd	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge \left(A\cap B\subseteq C\wedge C\subseteq A\right)\wedge \left(A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to C{𝑀}_{\mathscr{H}}D$$