chirredlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		chirred.1	$⊢ A \in C_{ℋ}$
2		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
3		chjcom	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
4	2 3	sylan	$⊢ (p \in HAtoms \land q \in C_{ℋ}) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
5	4	ad2ant2r	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
6	5	adantr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
7	6	ineq2d	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to ⊥ (r) \cap (p \lor_{ℋ} q) = ⊥ (r) \cap (q \lor_{ℋ} p)$
8		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
9		choccl	$⊢ r \in C_{ℋ} \to ⊥ (r) \in C_{ℋ}$
10	8 9	syl	$⊢ r \in HAtoms \to ⊥ (r) \in C_{ℋ}$
11		id	$⊢ q \in C_{ℋ} \to q \in C_{ℋ}$
12	10 11 2	3anim123i	$⊢ (r \in HAtoms \land q \in C_{ℋ} \land p \in HAtoms) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
13	12	3com13	$⊢ (p \in HAtoms \land q \in C_{ℋ} \land r \in HAtoms) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
14	13	3expa	$⊢ ((p \in HAtoms \land q \in C_{ℋ}) \land r \in HAtoms) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
15	14	adantllr	$⊢ (((p \in HAtoms \land p \subseteq A) \land q \in C_{ℋ}) \land r \in HAtoms) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
16	15	adantlrr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land r \in HAtoms) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
17	16	adantrr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq A)) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
18	17	adantrr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to (⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ})$
19		simpll	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land (r \in HAtoms \land r \subseteq A)) \to q \in C_{ℋ}$
20	10	ad2antrl	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land (r \in HAtoms \land r \subseteq A)) \to ⊥ (r) \in C_{ℋ}$
21		chsscon3	$⊢ (r \in C_{ℋ} \land A \in C_{ℋ}) \to (r \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (r))$
22	8 1 21	sylancl	$⊢ r \in HAtoms \to (r \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (r))$
23	22	biimpa	$⊢ (r \in HAtoms \land r \subseteq A) \to ⊥ (A) \subseteq ⊥ (r)$
24		sstr	$⊢ (q \subseteq ⊥ (A) \land ⊥ (A) \subseteq ⊥ (r)) \to q \subseteq ⊥ (r)$
25	23 24	sylan2	$⊢ (q \subseteq ⊥ (A) \land (r \in HAtoms \land r \subseteq A)) \to q \subseteq ⊥ (r)$
26	25	adantll	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land (r \in HAtoms \land r \subseteq A)) \to q \subseteq ⊥ (r)$
27		lecm	$⊢ (q \in C_{ℋ} \land ⊥ (r) \in C_{ℋ} \land q \subseteq ⊥ (r)) \to q 𝐶_{ℋ} ⊥ (r)$
28	19 20 26 27	syl3anc	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land (r \in HAtoms \land r \subseteq A)) \to q 𝐶_{ℋ} ⊥ (r)$
29	28	ad2ant2lr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to q 𝐶_{ℋ} ⊥ (r)$
30		chsscon3	$⊢ (p \in C_{ℋ} \land A \in C_{ℋ}) \to (p \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (p))$
31	1 30	mpan2	$⊢ p \in C_{ℋ} \to (p \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (p))$
32	31	biimpa	$⊢ (p \in C_{ℋ} \land p \subseteq A) \to ⊥ (A) \subseteq ⊥ (p)$
33		sstr	$⊢ (q \subseteq ⊥ (A) \land ⊥ (A) \subseteq ⊥ (p)) \to q \subseteq ⊥ (p)$
34	32 33	sylan2	$⊢ (q \subseteq ⊥ (A) \land (p \in C_{ℋ} \land p \subseteq A)) \to q \subseteq ⊥ (p)$
35	34	an12s	$⊢ (p \in C_{ℋ} \land (q \subseteq ⊥ (A) \land p \subseteq A)) \to q \subseteq ⊥ (p)$
36	35	ancom2s	$⊢ (p \in C_{ℋ} \land (p \subseteq A \land q \subseteq ⊥ (A))) \to q \subseteq ⊥ (p)$
37	36	adantll	$⊢ ((q \in C_{ℋ} \land p \in C_{ℋ}) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to q \subseteq ⊥ (p)$
38		choccl	$⊢ p \in C_{ℋ} \to ⊥ (p) \in C_{ℋ}$
39		lecm	$⊢ (q \in C_{ℋ} \land ⊥ (p) \in C_{ℋ} \land q \subseteq ⊥ (p)) \to q 𝐶_{ℋ} ⊥ (p)$
40	38 39	syl3an2	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ} \land q \subseteq ⊥ (p)) \to q 𝐶_{ℋ} ⊥ (p)$
41	40	3expia	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ}) \to (q \subseteq ⊥ (p) \to q 𝐶_{ℋ} ⊥ (p))$
42		cmcm2	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ}) \to (q 𝐶_{ℋ} p \leftrightarrow q 𝐶_{ℋ} ⊥ (p))$
43	41 42	sylibrd	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ}) \to (q \subseteq ⊥ (p) \to q 𝐶_{ℋ} p)$
44	43	adantr	$⊢ ((q \in C_{ℋ} \land p \in C_{ℋ}) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to (q \subseteq ⊥ (p) \to q 𝐶_{ℋ} p)$
45	37 44	mpd	$⊢ ((q \in C_{ℋ} \land p \in C_{ℋ}) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to q 𝐶_{ℋ} p$
46	2 45	sylanl2	$⊢ ((q \in C_{ℋ} \land p \in HAtoms) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to q 𝐶_{ℋ} p$
47	46	ancom1s	$⊢ ((p \in HAtoms \land q \in C_{ℋ}) \land (p \subseteq A \land q \subseteq ⊥ (A))) \to q 𝐶_{ℋ} p$
48	47	an4s	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to q 𝐶_{ℋ} p$
49	48	adantr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to q 𝐶_{ℋ} p$
50		fh2	$⊢ ((⊥ (r) \in C_{ℋ} \land q \in C_{ℋ} \land p \in C_{ℋ}) \land (q 𝐶_{ℋ} ⊥ (r) \land q 𝐶_{ℋ} p)) \to ⊥ (r) \cap (q \lor_{ℋ} p) = (⊥ (r) \cap q) \lor_{ℋ} (⊥ (r) \cap p)$
51	18 29 49 50	syl12anc	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to ⊥ (r) \cap (q \lor_{ℋ} p) = (⊥ (r) \cap q) \lor_{ℋ} (⊥ (r) \cap p)$
52		sseqin2	$⊢ q \subseteq ⊥ (r) \leftrightarrow ⊥ (r) \cap q = q$
53	26 52	sylib	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land (r \in HAtoms \land r \subseteq A)) \to ⊥ (r) \cap q = q$
54	53	ad2ant2lr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to ⊥ (r) \cap q = q$
55		incom	$⊢ ⊥ (r) \cap p = p \cap ⊥ (r)$
56	1	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_{ℋ}$
57	56	adantllr	$⊢ (((p \in HAtoms \land p \subseteq A) \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_{ℋ}$
58	55 57	syl5eq	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to ⊥ (r) \cap p = 0_{ℋ}$
59	54 58	oveq12d	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to (⊥ (r) \cap q) \lor_{ℋ} (⊥ (r) \cap p) = q \lor_{ℋ} 0_{ℋ}$
60		chj0	$⊢ q \in C_{ℋ} \to q \lor_{ℋ} 0_{ℋ} = q$
61	60	adantr	$⊢ (q \in C_{ℋ} \land q \subseteq ⊥ (A)) \to q \lor_{ℋ} 0_{ℋ} = q$
62	61	ad2antlr	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to q \lor_{ℋ} 0_{ℋ} = q$
63	59 62	eqtrd	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to (⊥ (r) \cap q) \lor_{ℋ} (⊥ (r) \cap p) = q$
64	7 51 63	3eqtrd	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to ⊥ (r) \cap (p \lor_{ℋ} q) = q$

Metamath Proof Explorer

Theorem chirredlem2

Proof