chirredlem1

Description: Lemma for chirredi . (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	chirred.1	$⊢ A \in C_{ℋ}$
	Assertion	chirredlem1	$⊢ ((p \in HAtoms \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to p \cap ⊥ (r) = 0_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		chirred.1	$⊢ A \in C_{ℋ}$
2		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
3		chsscon3	$⊢ (r \in C_{ℋ} \land A \in C_{ℋ}) \to (r \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (r))$
4	1 3	mpan2	$⊢ r \in C_{ℋ} \to (r \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (r))$
5	4	biimpa	$⊢ (r \in C_{ℋ} \land r \subseteq A) \to ⊥ (A) \subseteq ⊥ (r)$
6	2 5	sylan	$⊢ (r \in HAtoms \land r \subseteq A) \to ⊥ (A) \subseteq ⊥ (r)$
7		sstr2	$⊢ q \subseteq ⊥ (A) \to (⊥ (A) \subseteq ⊥ (r) \to q \subseteq ⊥ (r))$
8	6 7	syl5	$⊢ q \subseteq ⊥ (A) \to ((r \in HAtoms \land r \subseteq A) \to q \subseteq ⊥ (r))$
9		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
10		atne0	$⊢ r \in HAtoms \to r \neq 0_{ℋ}$
11	10	neneqd	$⊢ r \in HAtoms \to \neg r = 0_{ℋ}$
12	11	ad3antrrr	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \to \neg r = 0_{ℋ}$
13		simplr	$⊢ ((((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \land p \subseteq ⊥ (r)) \to r \subseteq p \lor_{ℋ} q$
14		choccl	$⊢ r \in C_{ℋ} \to ⊥ (r) \in C_{ℋ}$
15	2 14	syl	$⊢ r \in HAtoms \to ⊥ (r) \in C_{ℋ}$
16		chlej1	$⊢ ((p \in C_{ℋ} \land ⊥ (r) \in C_{ℋ} \land q \in C_{ℋ}) \land p \subseteq ⊥ (r)) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q$
17	16	3exp1	$⊢ p \in C_{ℋ} \to (⊥ (r) \in C_{ℋ} \to (q \in C_{ℋ} \to (p \subseteq ⊥ (r) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q)))$
18	15 17	syl5com	$⊢ r \in HAtoms \to (p \in C_{ℋ} \to (q \in C_{ℋ} \to (p \subseteq ⊥ (r) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q)))$
19	18	imp42	$⊢ ((r \in HAtoms \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land p \subseteq ⊥ (r)) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q$
20	19	adantllr	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land p \subseteq ⊥ (r)) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q$
21	20	adantlr	$⊢ ((((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \land p \subseteq ⊥ (r)) \to p \lor_{ℋ} q \subseteq ⊥ (r) \lor_{ℋ} q$
22	13 21	sstrd	$⊢ ((((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \land p \subseteq ⊥ (r)) \to r \subseteq ⊥ (r) \lor_{ℋ} q$
23		chlejb2	$⊢ (q \in C_{ℋ} \land ⊥ (r) \in C_{ℋ}) \to (q \subseteq ⊥ (r) \leftrightarrow ⊥ (r) \lor_{ℋ} q = ⊥ (r))$
24	23	ancoms	$⊢ (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ}) \to (q \subseteq ⊥ (r) \leftrightarrow ⊥ (r) \lor_{ℋ} q = ⊥ (r))$
25	24	biimpa	$⊢ ((⊥ (r) \in C_{ℋ} \land q \in C_{ℋ}) \land q \subseteq ⊥ (r)) \to ⊥ (r) \lor_{ℋ} q = ⊥ (r)$
26	15 25	sylanl1	$⊢ ((r \in HAtoms \land q \in C_{ℋ}) \land q \subseteq ⊥ (r)) \to ⊥ (r) \lor_{ℋ} q = ⊥ (r)$
27	26	an32s	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land q \in C_{ℋ}) \to ⊥ (r) \lor_{ℋ} q = ⊥ (r)$
28	27	adantrl	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \to ⊥ (r) \lor_{ℋ} q = ⊥ (r)$
29	28	ad2antrr	$⊢ ((((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \land p \subseteq ⊥ (r)) \to ⊥ (r) \lor_{ℋ} q = ⊥ (r)$
30	22 29	sseqtrd	$⊢ ((((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \land p \subseteq ⊥ (r)) \to r \subseteq ⊥ (r)$
31	30	ex	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq ⊥ (r) \to r \subseteq ⊥ (r))$
32		chssoc	$⊢ r \in C_{ℋ} \to (r \subseteq ⊥ (r) \leftrightarrow r = 0_{ℋ})$
33	32	biimpd	$⊢ r \in C_{ℋ} \to (r \subseteq ⊥ (r) \to r = 0_{ℋ})$
34	2 33	syl	$⊢ r \in HAtoms \to (r \subseteq ⊥ (r) \to r = 0_{ℋ})$
35	34	ad3antrrr	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \to (r \subseteq ⊥ (r) \to r = 0_{ℋ})$
36	31 35	syld	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq ⊥ (r) \to r = 0_{ℋ})$
37	12 36	mtod	$⊢ (((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \land r \subseteq p \lor_{ℋ} q) \to \neg p \subseteq ⊥ (r)$
38	37	ex	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in C_{ℋ} \land q \in C_{ℋ})) \to (r \subseteq p \lor_{ℋ} q \to \neg p \subseteq ⊥ (r))$
39	9 38	sylanr1	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in HAtoms \land q \in C_{ℋ})) \to (r \subseteq p \lor_{ℋ} q \to \neg p \subseteq ⊥ (r))$
40		atnssm0	$⊢ (⊥ (r) \in C_{ℋ} \land p \in HAtoms) \to (\neg p \subseteq ⊥ (r) \leftrightarrow ⊥ (r) \cap p = 0_{ℋ})$
41		incom	$⊢ ⊥ (r) \cap p = p \cap ⊥ (r)$
42	41	eqeq1i	$⊢ ⊥ (r) \cap p = 0_{ℋ} \leftrightarrow p \cap ⊥ (r) = 0_{ℋ}$
43	40 42	bitrdi	$⊢ (⊥ (r) \in C_{ℋ} \land p \in HAtoms) \to (\neg p \subseteq ⊥ (r) \leftrightarrow p \cap ⊥ (r) = 0_{ℋ})$
44	15 43	sylan	$⊢ (r \in HAtoms \land p \in HAtoms) \to (\neg p \subseteq ⊥ (r) \leftrightarrow p \cap ⊥ (r) = 0_{ℋ})$
45	44	ad2ant2r	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in HAtoms \land q \in C_{ℋ})) \to (\neg p \subseteq ⊥ (r) \leftrightarrow p \cap ⊥ (r) = 0_{ℋ})$
46	39 45	sylibd	$⊢ ((r \in HAtoms \land q \subseteq ⊥ (r)) \land (p \in HAtoms \land q \in C_{ℋ})) \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ})$
47	46	exp43	$⊢ r \in HAtoms \to (q \subseteq ⊥ (r) \to (p \in HAtoms \to (q \in C_{ℋ} \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ}))))$
48	47	adantr	$⊢ (r \in HAtoms \land r \subseteq A) \to (q \subseteq ⊥ (r) \to (p \in HAtoms \to (q \in C_{ℋ} \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ}))))$
49	8 48	sylcom	$⊢ q \subseteq ⊥ (A) \to ((r \in HAtoms \land r \subseteq A) \to (p \in HAtoms \to (q \in C_{ℋ} \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ}))))$
50	49	com4t	$⊢ p \in HAtoms \to (q \in C_{ℋ} \to (q \subseteq ⊥ (A) \to ((r \in HAtoms \land r \subseteq A) \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ}))))$
51	50	impd	$⊢ p \in HAtoms \to ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \to ((r \in HAtoms \land r \subseteq A) \to (r \subseteq p \lor_{ℋ} q \to p \cap ⊥ (r) = 0_{ℋ})))$
52	51	imp43	$⊢ ((p \in HAtoms \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to p \cap ⊥ (r) = 0_{ℋ}$

Metamath Proof Explorer

Theorem chirredlem1

Proof