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 C_{ℋ}$
	mdslmd.2	$⊢ B \in C_{ℋ}$
	mdslmd.3	$⊢ C \in C_{ℋ}$
	mdslmd.4	$⊢ D \in C_{ℋ}$
Assertion	mdslmd4i	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to C 𝑀_{ℋ} D$

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	$⊢ A \in C_{ℋ}$
2		mdslmd.2	$⊢ B \in C_{ℋ}$
3		mdslmd.3	$⊢ C \in C_{ℋ}$
4		mdslmd.4	$⊢ D \in C_{ℋ}$
5		simp1	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to A 𝑀_{ℋ} B$
6	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
7		ssmd1	$⊢ (A \cap B \in C_{ℋ} \land D \in C_{ℋ} \land A \cap B \subseteq D) \to (A \cap B) 𝑀_{ℋ} D$
8	6 4 7	mp3an12	$⊢ A \cap B \subseteq D \to (A \cap B) 𝑀_{ℋ} D$
9	8	adantr	$⊢ (A \cap B \subseteq D \land D \subseteq B) \to (A \cap B) 𝑀_{ℋ} D$
10	9	3ad2ant3	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to (A \cap B) 𝑀_{ℋ} D$
11		sslin	$⊢ D \subseteq B \to A \cap D \subseteq A \cap B$
12		sstr	$⊢ (A \cap D \subseteq A \cap B \land A \cap B \subseteq C) \to A \cap D \subseteq C$
13	11 12	sylan	$⊢ (D \subseteq B \land A \cap B \subseteq C) \to A \cap D \subseteq C$
14	13	ancoms	$⊢ (A \cap B \subseteq C \land D \subseteq B) \to A \cap D \subseteq C$
15	14	ad2ant2rl	$⊢ ((A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to A \cap D \subseteq C$
16	15	3adant1	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to A \cap D \subseteq C$
17		simp2r	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to C \subseteq A$
18	1 2 4 3	mdslmd3i	$⊢ ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} D) \land (A \cap D \subseteq C \land C \subseteq A)) \to C 𝑀_{ℋ} (B \cap D)$
19	5 10 16 17 18	syl22anc	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to C 𝑀_{ℋ} (B \cap D)$
20		sseqin2	$⊢ D \subseteq B \leftrightarrow B \cap D = D$
21	20	biimpi	$⊢ D \subseteq B \to B \cap D = D$
22	21	adantl	$⊢ (A \cap B \subseteq D \land D \subseteq B) \to B \cap D = D$
23	22	3ad2ant3	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to B \cap D = D$
24	19 23	breqtrd	$⊢ (A 𝑀_{ℋ} B \land (A \cap B \subseteq C \land C \subseteq A) \land (A \cap B \subseteq D \land D \subseteq B)) \to C 𝑀_{ℋ} D$

Metamath Proof Explorer

Theorem mdslmd4i

Proof