atabsi

Description: Absorption of an incomparable atom. Similar to Exercise 7.1 of MaedaMaeda p. 34. (Contributed by NM, 15-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atabs.1	$⊢ A \in C_{ℋ}$
	atabs.2	$⊢ B \in C_{ℋ}$
Assertion	atabsi	$⊢ C \in HAtoms \to (\neg C \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} C) \cap B = A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		atabs.1	$⊢ A \in C_{ℋ}$
2		atabs.2	$⊢ B \in C_{ℋ}$
3		inass	$⊢ ((A \lor_{ℋ} C) \cap (A \lor_{ℋ} B)) \cap B = (A \lor_{ℋ} C) \cap ((A \lor_{ℋ} B) \cap B)$
4	1 2	chjcomi	$⊢ A \lor_{ℋ} B = B \lor_{ℋ} A$
5	4	ineq1i	$⊢ (A \lor_{ℋ} B) \cap B = (B \lor_{ℋ} A) \cap B$
6		incom	$⊢ (B \lor_{ℋ} A) \cap B = B \cap (B \lor_{ℋ} A)$
7	2 1	chabs2i	$⊢ B \cap (B \lor_{ℋ} A) = B$
8	5 6 7	3eqtri	$⊢ (A \lor_{ℋ} B) \cap B = B$
9	8	ineq2i	$⊢ (A \lor_{ℋ} C) \cap ((A \lor_{ℋ} B) \cap B) = (A \lor_{ℋ} C) \cap B$
10	3 9	eqtr2i	$⊢ (A \lor_{ℋ} C) \cap B = ((A \lor_{ℋ} C) \cap (A \lor_{ℋ} B)) \cap B$
11	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
12		atelch	$⊢ C \in HAtoms \to C \in C_{ℋ}$
13	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
14		atmd	$⊢ (C \in HAtoms \land A \lor_{ℋ} B \in C_{ℋ}) \to C 𝑀_{ℋ} (A \lor_{ℋ} B)$
15	13 14	mpan2	$⊢ C \in HAtoms \to C 𝑀_{ℋ} (A \lor_{ℋ} B)$
16		mdi	$⊢ ((C \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ} \land A \in C_{ℋ}) \land (C 𝑀_{ℋ} (A \lor_{ℋ} B) \land A \subseteq A \lor_{ℋ} B)) \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B))$
17	16	exp32	$⊢ (C \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ} \land A \in C_{ℋ}) \to (C 𝑀_{ℋ} (A \lor_{ℋ} B) \to (A \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B))))$
18	13 1 17	mp3an23	$⊢ C \in C_{ℋ} \to (C 𝑀_{ℋ} (A \lor_{ℋ} B) \to (A \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B))))$
19	12 15 18	sylc	$⊢ C \in HAtoms \to (A \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B)))$
20	11 19	mpi	$⊢ C \in HAtoms \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B))$
21	20	adantr	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A \lor_{ℋ} (C \cap (A \lor_{ℋ} B))$
22		incom	$⊢ C \cap (A \lor_{ℋ} B) = (A \lor_{ℋ} B) \cap C$
23		atnssm0	$⊢ (A \lor_{ℋ} B \in C_{ℋ} \land C \in HAtoms) \to (\neg C \subseteq A \lor_{ℋ} B \leftrightarrow (A \lor_{ℋ} B) \cap C = 0_{ℋ})$
24	13 23	mpan	$⊢ C \in HAtoms \to (\neg C \subseteq A \lor_{ℋ} B \leftrightarrow (A \lor_{ℋ} B) \cap C = 0_{ℋ})$
25	24	biimpa	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to (A \lor_{ℋ} B) \cap C = 0_{ℋ}$
26	22 25	syl5eq	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to C \cap (A \lor_{ℋ} B) = 0_{ℋ}$
27	26	oveq2d	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to A \lor_{ℋ} (C \cap (A \lor_{ℋ} B)) = A \lor_{ℋ} 0_{ℋ}$
28	1	chj0i	$⊢ A \lor_{ℋ} 0_{ℋ} = A$
29	27 28	eqtrdi	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to A \lor_{ℋ} (C \cap (A \lor_{ℋ} B)) = A$
30	21 29	eqtrd	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to (A \lor_{ℋ} C) \cap (A \lor_{ℋ} B) = A$
31	30	ineq1d	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to ((A \lor_{ℋ} C) \cap (A \lor_{ℋ} B)) \cap B = A \cap B$
32	10 31	syl5eq	$⊢ (C \in HAtoms \land \neg C \subseteq A \lor_{ℋ} B) \to (A \lor_{ℋ} C) \cap B = A \cap B$
33	32	ex	$⊢ C \in HAtoms \to (\neg C \subseteq A \lor_{ℋ} B \to (A \lor_{ℋ} C) \cap B = A \cap B)$

Metamath Proof Explorer

Theorem atabsi

Proof