chirredlem3

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

	Ref	Expression
Hypotheses	chirred.1	$⊢ A \in C_{ℋ}$
	chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
Assertion	chirredlem3	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq A \to r = p)$

Proof

Step	Hyp	Ref	Expression
1		chirred.1	$⊢ A \in C_{ℋ}$
2		chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
3		atelch	$⊢ q \in HAtoms \to q \in C_{ℋ}$
4	1	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$
5	4	oveq2d	$⊢ (((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 \lor_{ℋ} (⊥ (r) \cap (p \lor_{ℋ} q)) = r \lor_{ℋ} q$
6		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
7	6	adantr	$⊢ (r \in HAtoms \land r \subseteq A) \to r \in C_{ℋ}$
8		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
9		chjcl	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to p \lor_{ℋ} q \in C_{ℋ}$
10	8 9	sylan	$⊢ (p \in HAtoms \land q \in C_{ℋ}) \to p \lor_{ℋ} q \in C_{ℋ}$
11	10	ad2ant2r	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to p \lor_{ℋ} q \in C_{ℋ}$
12		id	$⊢ r \subseteq p \lor_{ℋ} q \to r \subseteq p \lor_{ℋ} q$
13		pjoml2	$⊢ (r \in C_{ℋ} \land p \lor_{ℋ} q \in C_{ℋ} \land r \subseteq p \lor_{ℋ} q) \to r \lor_{ℋ} (⊥ (r) \cap (p \lor_{ℋ} q)) = p \lor_{ℋ} q$
14	7 11 12 13	syl3an	$⊢ ((r \in HAtoms \land r \subseteq A) \land ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \land r \subseteq p \lor_{ℋ} q) \to r \lor_{ℋ} (⊥ (r) \cap (p \lor_{ℋ} q)) = p \lor_{ℋ} q$
15	14	3com12	$⊢ (((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 \lor_{ℋ} (⊥ (r) \cap (p \lor_{ℋ} q)) = p \lor_{ℋ} q$
16	15	3expb	$⊢ (((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 \lor_{ℋ} (⊥ (r) \cap (p \lor_{ℋ} q)) = p \lor_{ℋ} q$
17	5 16	eqtr3d	$⊢ (((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 \lor_{ℋ} q = p \lor_{ℋ} q$
18	17	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 A \cap (r \lor_{ℋ} q) = A \cap (p \lor_{ℋ} q)$
19		breq2	$⊢ x = r \to (A 𝐶_{ℋ} x \leftrightarrow A 𝐶_{ℋ} r)$
20	19 2	vtoclga	$⊢ r \in C_{ℋ} \to A 𝐶_{ℋ} r$
21		breq2	$⊢ x = q \to (A 𝐶_{ℋ} x \leftrightarrow A 𝐶_{ℋ} q)$
22	21 2	vtoclga	$⊢ q \in C_{ℋ} \to A 𝐶_{ℋ} q$
23	20 22	anim12i	$⊢ (r \in C_{ℋ} \land q \in C_{ℋ}) \to (A 𝐶_{ℋ} r \land A 𝐶_{ℋ} q)$
24		fh1	$⊢ ((A \in C_{ℋ} \land r \in C_{ℋ} \land q \in C_{ℋ}) \land (A 𝐶_{ℋ} r \land A 𝐶_{ℋ} q)) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
25	1 24	mp3anl1	$⊢ ((r \in C_{ℋ} \land q \in C_{ℋ}) \land (A 𝐶_{ℋ} r \land A 𝐶_{ℋ} q)) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
26	23 25	mpdan	$⊢ (r \in C_{ℋ} \land q \in C_{ℋ}) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
27	6 26	sylan	$⊢ (r \in HAtoms \land q \in C_{ℋ}) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
28	27	ancoms	$⊢ (q \in C_{ℋ} \land r \in HAtoms) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
29	28	adantrr	$⊢ (q \in C_{ℋ} \land (r \in HAtoms \land r \subseteq A)) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
30	29	ad2ant2r	$⊢ ((q \in C_{ℋ} \land q \subseteq ⊥ (A)) \land ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q)) \to A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
31	30	adantll	$⊢ (((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 A \cap (r \lor_{ℋ} q) = (A \cap r) \lor_{ℋ} (A \cap q)$
32		breq2	$⊢ x = p \to (A 𝐶_{ℋ} x \leftrightarrow A 𝐶_{ℋ} p)$
33	32 2	vtoclga	$⊢ p \in C_{ℋ} \to A 𝐶_{ℋ} p$
34	33 22	anim12i	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to (A 𝐶_{ℋ} p \land A 𝐶_{ℋ} q)$
35		fh1	$⊢ ((A \in C_{ℋ} \land p \in C_{ℋ} \land q \in C_{ℋ}) \land (A 𝐶_{ℋ} p \land A 𝐶_{ℋ} q)) \to A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
36	1 35	mp3anl1	$⊢ ((p \in C_{ℋ} \land q \in C_{ℋ}) \land (A 𝐶_{ℋ} p \land A 𝐶_{ℋ} q)) \to A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
37	34 36	mpdan	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
38	8 37	sylan	$⊢ (p \in HAtoms \land q \in C_{ℋ}) \to A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
39	38	ad2ant2r	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
40	39	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 A \cap (p \lor_{ℋ} q) = (A \cap p) \lor_{ℋ} (A \cap q)$
41	18 31 40	3eqtr3d	$⊢ (((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 (A \cap r) \lor_{ℋ} (A \cap q) = (A \cap p) \lor_{ℋ} (A \cap q)$
42		sseqin2	$⊢ r \subseteq A \leftrightarrow A \cap r = r$
43	42	biimpi	$⊢ r \subseteq A \to A \cap r = r$
44	43	ad2antlr	$⊢ ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q) \to A \cap r = r$
45	44	adantl	$⊢ (((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 A \cap r = r$
46		incom	$⊢ A \cap q = q \cap A$
47		chsh	$⊢ q \in C_{ℋ} \to q \in S_{ℋ}$
48	1	chshii	$⊢ A \in S_{ℋ}$
49		orthin	$⊢ (q \in S_{ℋ} \land A \in S_{ℋ}) \to (q \subseteq ⊥ (A) \to q \cap A = 0_{ℋ})$
50	47 48 49	sylancl	$⊢ q \in C_{ℋ} \to (q \subseteq ⊥ (A) \to q \cap A = 0_{ℋ})$
51	50	imp	$⊢ (q \in C_{ℋ} \land q \subseteq ⊥ (A)) \to q \cap A = 0_{ℋ}$
52	46 51	syl5eq	$⊢ (q \in C_{ℋ} \land q \subseteq ⊥ (A)) \to A \cap q = 0_{ℋ}$
53	52	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 A \cap q = 0_{ℋ}$
54	45 53	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 (A \cap r) \lor_{ℋ} (A \cap q) = r \lor_{ℋ} 0_{ℋ}$
55		sseqin2	$⊢ p \subseteq A \leftrightarrow A \cap p = p$
56	55	biimpi	$⊢ p \subseteq A \to A \cap p = p$
57	56	adantl	$⊢ (p \in HAtoms \land p \subseteq A) \to A \cap p = p$
58	57	ad2antrr	$⊢ (((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 A \cap p = p$
59	58 53	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 (A \cap p) \lor_{ℋ} (A \cap q) = p \lor_{ℋ} 0_{ℋ}$
60	41 54 59	3eqtr3d	$⊢ (((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 \lor_{ℋ} 0_{ℋ} = p \lor_{ℋ} 0_{ℋ}$
61		chj0	$⊢ r \in C_{ℋ} \to r \lor_{ℋ} 0_{ℋ} = r$
62	6 61	syl	$⊢ r \in HAtoms \to r \lor_{ℋ} 0_{ℋ} = r$
63	62	ad2antrr	$⊢ ((r \in HAtoms \land r \subseteq A) \land r \subseteq p \lor_{ℋ} q) \to r \lor_{ℋ} 0_{ℋ} = r$
64	63	adantl	$⊢ (((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 \lor_{ℋ} 0_{ℋ} = r$
65		chj0	$⊢ p \in C_{ℋ} \to p \lor_{ℋ} 0_{ℋ} = p$
66	8 65	syl	$⊢ p \in HAtoms \to p \lor_{ℋ} 0_{ℋ} = p$
67	66	ad3antrrr	$⊢ (((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_{ℋ} 0_{ℋ} = p$
68	60 64 67	3eqtr3d	$⊢ (((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 = p$
69	68	exp44	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to (r \in HAtoms \to (r \subseteq A \to (r \subseteq p \lor_{ℋ} q \to r = p)))$
70	69	com34	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in C_{ℋ} \land q \subseteq ⊥ (A))) \to (r \in HAtoms \to (r \subseteq p \lor_{ℋ} q \to (r \subseteq A \to r = p)))$
71	3 70	sylanr1	$⊢ ((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \to (r \in HAtoms \to (r \subseteq p \lor_{ℋ} q \to (r \subseteq A \to r = p)))$
72	71	imp32	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq A \to r = p)$

Metamath Proof Explorer

Theorem chirredlem3

Proof