mdsl0

Description: A sublattice condition that transfers the modular pair property. Exercise 12 of Kalmbach p. 103. Also Lemma 1.5.3 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	mdsl0	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \to ((((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ}) \land A 𝑀_{ℋ} B) \to C 𝑀_{ℋ} D)$

Proof

Step	Hyp	Ref	Expression
1		sstr2	$⊢ x \subseteq D \to (D \subseteq B \to x \subseteq B)$
2	1	com12	$⊢ D \subseteq B \to (x \subseteq D \to x \subseteq B)$
3	2	ad2antlr	$⊢ ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ}) \to (x \subseteq D \to x \subseteq B)$
4	3	ad2antlr	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \land x \in C_{ℋ}) \to (x \subseteq D \to x \subseteq B)$
5		chlej2	$⊢ ((C \in C_{ℋ} \land A \in C_{ℋ} \land x \in C_{ℋ}) \land C \subseteq A) \to x \lor_{ℋ} C \subseteq x \lor_{ℋ} A$
6		ss2in	$⊢ (x \lor_{ℋ} C \subseteq x \lor_{ℋ} A \land D \subseteq B) \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B$
7	6	ex	$⊢ x \lor_{ℋ} C \subseteq x \lor_{ℋ} A \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B)$
8	5 7	syl	$⊢ ((C \in C_{ℋ} \land A \in C_{ℋ} \land x \in C_{ℋ}) \land C \subseteq A) \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B)$
9	8	ex	$⊢ (C \in C_{ℋ} \land A \in C_{ℋ} \land x \in C_{ℋ}) \to (C \subseteq A \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B))$
10	9	3expia	$⊢ (C \in C_{ℋ} \land A \in C_{ℋ}) \to (x \in C_{ℋ} \to (C \subseteq A \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B)))$
11	10	ancoms	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (x \in C_{ℋ} \to (C \subseteq A \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B)))$
12	11	ad2ant2r	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \to (x \in C_{ℋ} \to (C \subseteq A \to (D \subseteq B \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B)))$
13	12	imp43	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land x \in C_{ℋ}) \land (C \subseteq A \land D \subseteq B)) \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B$
14	13	adantrr	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land x \in C_{ℋ}) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B$
15		oveq2	$⊢ A \cap B = 0_{ℋ} \to x \lor_{ℋ} (A \cap B) = x \lor_{ℋ} 0_{ℋ}$
16		chj0	$⊢ x \in C_{ℋ} \to x \lor_{ℋ} 0_{ℋ} = x$
17	15 16	sylan9eqr	$⊢ (x \in C_{ℋ} \land A \cap B = 0_{ℋ}) \to x \lor_{ℋ} (A \cap B) = x$
18	17	adantl	$⊢ ((C \in C_{ℋ} \land D \in C_{ℋ}) \land (x \in C_{ℋ} \land A \cap B = 0_{ℋ})) \to x \lor_{ℋ} (A \cap B) = x$
19		chincl	$⊢ (C \in C_{ℋ} \land D \in C_{ℋ}) \to C \cap D \in C_{ℋ}$
20		chub1	$⊢ (x \in C_{ℋ} \land C \cap D \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} (C \cap D)$
21	20	ancoms	$⊢ (C \cap D \in C_{ℋ} \land x \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} (C \cap D)$
22	19 21	sylan	$⊢ ((C \in C_{ℋ} \land D \in C_{ℋ}) \land x \in C_{ℋ}) \to x \subseteq x \lor_{ℋ} (C \cap D)$
23	22	adantrr	$⊢ ((C \in C_{ℋ} \land D \in C_{ℋ}) \land (x \in C_{ℋ} \land A \cap B = 0_{ℋ})) \to x \subseteq x \lor_{ℋ} (C \cap D)$
24	18 23	eqsstrd	$⊢ ((C \in C_{ℋ} \land D \in C_{ℋ}) \land (x \in C_{ℋ} \land A \cap B = 0_{ℋ})) \to x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D)$
25	24	adantll	$⊢ (((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land (x \in C_{ℋ} \land A \cap B = 0_{ℋ})) \to x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D)$
26	25	anassrs	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land x \in C_{ℋ}) \land A \cap B = 0_{ℋ}) \to x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D)$
27	26	adantrl	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land x \in C_{ℋ}) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D)$
28		sstr2	$⊢ (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B \to ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (A \cap B))$
29		sstr2	$⊢ (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D))$
30	28 29	syl6	$⊢ (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B \to ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
31	30	com23	$⊢ (x \lor_{ℋ} C) \cap D \subseteq (x \lor_{ℋ} A) \cap B \to (x \lor_{ℋ} (A \cap B) \subseteq x \lor_{ℋ} (C \cap D) \to ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
32	14 27 31	sylc	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land x \in C_{ℋ}) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D))$
33	32	an32s	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \land x \in C_{ℋ}) \to ((x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B) \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D))$
34	4 33	imim12d	$⊢ ((((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \land x \in C_{ℋ}) \to ((x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)) \to (x \subseteq D \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
35	34	ralimdva	$⊢ (((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to (\forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)) \to \forall x \in C_{ℋ} (x \subseteq D \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
36		mdbr2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
37	36	ad2antrr	$⊢ (((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to (A 𝑀_{ℋ} B \leftrightarrow \forall x \in C_{ℋ} (x \subseteq B \to (x \lor_{ℋ} A) \cap B \subseteq x \lor_{ℋ} (A \cap B)))$
38		mdbr2	$⊢ (C \in C_{ℋ} \land D \in C_{ℋ}) \to (C 𝑀_{ℋ} D \leftrightarrow \forall x \in C_{ℋ} (x \subseteq D \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
39	38	ad2antlr	$⊢ (((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to (C 𝑀_{ℋ} D \leftrightarrow \forall x \in C_{ℋ} (x \subseteq D \to (x \lor_{ℋ} C) \cap D \subseteq x \lor_{ℋ} (C \cap D)))$
40	35 37 39	3imtr4d	$⊢ (((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \land ((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ})) \to (A 𝑀_{ℋ} B \to C 𝑀_{ℋ} D)$
41	40	expimpd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (C \in C_{ℋ} \land D \in C_{ℋ})) \to ((((C \subseteq A \land D \subseteq B) \land A \cap B = 0_{ℋ}) \land A 𝑀_{ℋ} B) \to C 𝑀_{ℋ} D)$

Metamath Proof Explorer

Theorem mdsl0

Proof