dmdbr6ati

Description: Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	$⊢ A \in C_{ℋ}$
	sumdmdi.2	$⊢ B \in C_{ℋ}$
Assertion	dmdbr6ati	$⊢ A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	$⊢ A \in C_{ℋ}$
2		sumdmdi.2	$⊢ B \in C_{ℋ}$
3		dmdbr3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B))$
4	1 2 3	mp2an	$⊢ A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)$
5		chabs2	$⊢ (x \in C_{ℋ} \land B \in C_{ℋ}) \to x \cap (x \lor_{ℋ} B) = x$
6	2 5	mpan2	$⊢ x \in C_{ℋ} \to x \cap (x \lor_{ℋ} B) = x$
7	6	ineq2d	$⊢ x \in C_{ℋ} \to (A \lor_{ℋ} B) \cap (x \cap (x \lor_{ℋ} B)) = (A \lor_{ℋ} B) \cap x$
8		incom	$⊢ (A \lor_{ℋ} B) \cap (x \cap (x \lor_{ℋ} B)) = (x \cap (x \lor_{ℋ} B)) \cap (A \lor_{ℋ} B)$
9		inass	$⊢ (x \cap (x \lor_{ℋ} B)) \cap (A \lor_{ℋ} B) = x \cap ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B))$
10		incom	$⊢ x \cap ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
11	8 9 10	3eqtri	$⊢ (A \lor_{ℋ} B) \cap (x \cap (x \lor_{ℋ} B)) = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
12	7 11	eqtr3di	$⊢ x \in C_{ℋ} \to (A \lor_{ℋ} B) \cap x = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
13	12	adantr	$⊢ (x \in C_{ℋ} \land ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \to (A \lor_{ℋ} B) \cap x = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
14		ineq1	$⊢ ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
15	14	adantl	$⊢ (x \in C_{ℋ} \land ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \to (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x = ((x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \cap x$
16	13 15	eqtr4d	$⊢ (x \in C_{ℋ} \land ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B)) \to (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$
17	16	ralimiaa	$⊢ \forall x \in C_{ℋ} ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B = (x \lor_{ℋ} B) \cap (A \lor_{ℋ} B) \to \forall x \in C_{ℋ} (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$
18	4 17	sylbi	$⊢ A 𝑀_{ℋ}^{*} B \to \forall x \in C_{ℋ} (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$
19		atelch	$⊢ x \in HAtoms \to x \in C_{ℋ}$
20	19	imim1i	$⊢ (x \in C_{ℋ} \to (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x) \to (x \in HAtoms \to (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x)$
21	20	ralimi2	$⊢ \forall x \in C_{ℋ} (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$
22	18 21	syl	$⊢ A 𝑀_{ℋ}^{*} B \to \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$
23		inss1	$⊢ (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B$
24		sseq1	$⊢ (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to ((A \lor_{ℋ} B) \cap x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \leftrightarrow (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
25	23 24	mpbiri	$⊢ (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to (A \lor_{ℋ} B) \cap x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B$
26		incom	$⊢ (A \lor_{ℋ} B) \cap x = x \cap (A \lor_{ℋ} B)$
27		df-ss	$⊢ x \subseteq A \lor_{ℋ} B \leftrightarrow x \cap (A \lor_{ℋ} B) = x$
28	27	biimpi	$⊢ x \subseteq A \lor_{ℋ} B \to x \cap (A \lor_{ℋ} B) = x$
29	26 28	syl5eq	$⊢ x \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} B) \cap x = x$
30	29	sseq1d	$⊢ x \subseteq A \lor_{ℋ} B \to ((A \lor_{ℋ} B) \cap x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B \leftrightarrow x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
31	25 30	syl5ibcom	$⊢ (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
32	31	ralimi	$⊢ \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to \forall x \in HAtoms (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
33	1 2	dmdbr5ati	$⊢ A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in HAtoms (x \subseteq A \lor_{ℋ} B \to x \subseteq ((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B)$
34	32 33	sylibr	$⊢ \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x \to A 𝑀_{ℋ}^{*} B$
35	22 34	impbii	$⊢ A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in HAtoms (A \lor_{ℋ} B) \cap x = (((x \lor_{ℋ} B) \cap A) \lor_{ℋ} B) \cap x$

Metamath Proof Explorer

Theorem dmdbr6ati

Proof