mdslmd3i

Description: Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of MaedaMaeda p. 2. (Contributed by NM, 23-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	mdslmd3i	$⊢ ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \to D 𝑀_{ℋ} (B \cap C)$

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		chlej2	$⊢ ((D \in C_{ℋ} \land A \in C_{ℋ} \land x \in C_{ℋ}) \land D \subseteq A) \to x \lor_{ℋ} D \subseteq x \lor_{ℋ} A$
6	5	ex	$⊢ (D \in C_{ℋ} \land A \in C_{ℋ} \land x \in C_{ℋ}) \to (D \subseteq A \to x \lor_{ℋ} D \subseteq x \lor_{ℋ} A)$
7	4 1 6	mp3an12	$⊢ x \in C_{ℋ} \to (D \subseteq A \to x \lor_{ℋ} D \subseteq x \lor_{ℋ} A)$
8	7	impcom	$⊢ (D \subseteq A \land x \in C_{ℋ}) \to x \lor_{ℋ} D \subseteq x \lor_{ℋ} A$
9	8	ssrind	$⊢ (D \subseteq A \land x \in C_{ℋ}) \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq (x \lor_{ℋ} A) \cap (B \cap C)$
10	9	adantll	$⊢ ((A \cap C \subseteq D \land D \subseteq A) \land x \in C_{ℋ}) \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq (x \lor_{ℋ} A) \cap (B \cap C)$
11	10	adantll	$⊢ (((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq (x \lor_{ℋ} A) \cap (B \cap C)$
12	11	adantr	$⊢ ((((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq (x \lor_{ℋ} A) \cap (B \cap C)$
13		ssin	$⊢ (x \subseteq B \land x \subseteq C) \leftrightarrow x \subseteq B \cap C$
14		inass	$⊢ ((x \lor_{ℋ} A) \cap B) \cap C = (x \lor_{ℋ} A) \cap (B \cap C)$
15		mdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land x \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land x \subseteq B)) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)$
16	1 15	mp3anl1	$⊢ ((B \in C_{ℋ} \land x \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land x \subseteq B)) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)$
17	2 16	mpanl1	$⊢ (x \in C_{ℋ} \land (A 𝑀_{ℋ} B \land x \subseteq B)) \to (x \lor_{ℋ} A) \cap B = x \lor_{ℋ} (A \cap B)$
18	17	ineq1d	$⊢ (x \in C_{ℋ} \land (A 𝑀_{ℋ} B \land x \subseteq B)) \to ((x \lor_{ℋ} A) \cap B) \cap C = (x \lor_{ℋ} (A \cap B)) \cap C$
19	14 18	eqtr3id	$⊢ (x \in C_{ℋ} \land (A 𝑀_{ℋ} B \land x \subseteq B)) \to (x \lor_{ℋ} A) \cap (B \cap C) = (x \lor_{ℋ} (A \cap B)) \cap C$
20	19	adantrlr	$⊢ (x \in C_{ℋ} \land ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land x \subseteq B)) \to (x \lor_{ℋ} A) \cap (B \cap C) = (x \lor_{ℋ} (A \cap B)) \cap C$
21	20	adantrrr	$⊢ (x \in C_{ℋ} \land ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (x \subseteq B \land x \subseteq C))) \to (x \lor_{ℋ} A) \cap (B \cap C) = (x \lor_{ℋ} (A \cap B)) \cap C$
22	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
23		mdi	$⊢ ((A \cap B \in C_{ℋ} \land C \in C_{ℋ} \land x \in C_{ℋ}) \land ((A \cap B) 𝑀_{ℋ} C \land x \subseteq C)) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} ((A \cap B) \cap C)$
24	22 23	mp3anl1	$⊢ ((C \in C_{ℋ} \land x \in C_{ℋ}) \land ((A \cap B) 𝑀_{ℋ} C \land x \subseteq C)) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} ((A \cap B) \cap C)$
25	3 24	mpanl1	$⊢ (x \in C_{ℋ} \land ((A \cap B) 𝑀_{ℋ} C \land x \subseteq C)) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} ((A \cap B) \cap C)$
26		inass	$⊢ (A \cap B) \cap C = A \cap (B \cap C)$
27	26	oveq2i	$⊢ x \lor_{ℋ} ((A \cap B) \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
28	25 27	eqtrdi	$⊢ (x \in C_{ℋ} \land ((A \cap B) 𝑀_{ℋ} C \land x \subseteq C)) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} (A \cap (B \cap C))$
29	28	adantrll	$⊢ (x \in C_{ℋ} \land ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land x \subseteq C)) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} (A \cap (B \cap C))$
30	29	adantrrl	$⊢ (x \in C_{ℋ} \land ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (x \subseteq B \land x \subseteq C))) \to (x \lor_{ℋ} (A \cap B)) \cap C = x \lor_{ℋ} (A \cap (B \cap C))$
31	21 30	eqtrd	$⊢ (x \in C_{ℋ} \land ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (x \subseteq B \land x \subseteq C))) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
32	31	ancoms	$⊢ (((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (x \subseteq B \land x \subseteq C)) \land x \in C_{ℋ}) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
33	32	an32s	$⊢ (((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land x \in C_{ℋ}) \land (x \subseteq B \land x \subseteq C)) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
34	13 33	sylan2br	$⊢ (((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
35	34	adantllr	$⊢ ((((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (A \cap (B \cap C))$
36		inass	$⊢ (A \cap C) \cap (B \cap C) = A \cap (C \cap (B \cap C))$
37		in12	$⊢ C \cap (B \cap C) = B \cap (C \cap C)$
38		inidm	$⊢ C \cap C = C$
39	38	ineq2i	$⊢ B \cap (C \cap C) = B \cap C$
40	37 39	eqtri	$⊢ C \cap (B \cap C) = B \cap C$
41	40	ineq2i	$⊢ A \cap (C \cap (B \cap C)) = A \cap (B \cap C)$
42	36 41	eqtr2i	$⊢ A \cap (B \cap C) = (A \cap C) \cap (B \cap C)$
43		ssrin	$⊢ A \cap C \subseteq D \to (A \cap C) \cap (B \cap C) \subseteq D \cap (B \cap C)$
44	42 43	eqsstrid	$⊢ A \cap C \subseteq D \to A \cap (B \cap C) \subseteq D \cap (B \cap C)$
45		ssrin	$⊢ D \subseteq A \to D \cap (B \cap C) \subseteq A \cap (B \cap C)$
46	44 45	anim12i	$⊢ (A \cap C \subseteq D \land D \subseteq A) \to (A \cap (B \cap C) \subseteq D \cap (B \cap C) \land D \cap (B \cap C) \subseteq A \cap (B \cap C))$
47		eqss	$⊢ A \cap (B \cap C) = D \cap (B \cap C) \leftrightarrow (A \cap (B \cap C) \subseteq D \cap (B \cap C) \land D \cap (B \cap C) \subseteq A \cap (B \cap C))$
48	46 47	sylibr	$⊢ (A \cap C \subseteq D \land D \subseteq A) \to A \cap (B \cap C) = D \cap (B \cap C)$
49	48	oveq2d	$⊢ (A \cap C \subseteq D \land D \subseteq A) \to x \lor_{ℋ} (A \cap (B \cap C)) = x \lor_{ℋ} (D \cap (B \cap C))$
50	49	ad3antlr	$⊢ ((((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to x \lor_{ℋ} (A \cap (B \cap C)) = x \lor_{ℋ} (D \cap (B \cap C))$
51	35 50	eqtrd	$⊢ ((((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to (x \lor_{ℋ} A) \cap (B \cap C) = x \lor_{ℋ} (D \cap (B \cap C))$
52	12 51	sseqtrd	$⊢ ((((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \land x \subseteq B \cap C) \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq x \lor_{ℋ} (D \cap (B \cap C))$
53	52	ex	$⊢ (((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \land x \in C_{ℋ}) \to (x \subseteq B \cap C \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq x \lor_{ℋ} (D \cap (B \cap C)))$
54	53	ralrimiva	$⊢ ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \to \forall x \in C_{ℋ} (x \subseteq B \cap C \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq x \lor_{ℋ} (D \cap (B \cap C)))$
55	2 3	chincli	$⊢ B \cap C \in C_{ℋ}$
56		mdbr2	$⊢ (D \in C_{ℋ} \land B \cap C \in C_{ℋ}) \to (D 𝑀_{ℋ} (B \cap C) \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \cap C \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq x \lor_{ℋ} (D \cap (B \cap C))))$
57	4 55 56	mp2an	$⊢ D 𝑀_{ℋ} (B \cap C) \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \cap C \to (x \lor_{ℋ} D) \cap (B \cap C) \subseteq x \lor_{ℋ} (D \cap (B \cap C)))$
58	54 57	sylibr	$⊢ ((A 𝑀_{ℋ} B \land (A \cap B) 𝑀_{ℋ} C) \land (A \cap C \subseteq D \land D \subseteq A)) \to D 𝑀_{ℋ} (B \cap C)$

Metamath Proof Explorer

Theorem mdslmd3i

Proof