osumcllem9N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
	osumcllem.a	$⊢ A = Atoms (K)$
	osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	osumcllem.c	$⊢ C = PSubCl (K)$
	osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
	osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
Assertion	osumcllem9N	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to M = X$

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		osumcllem.a	$⊢ A = Atoms (K)$
4		osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		osumcllem.c	$⊢ C = PSubCl (K)$
7		osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
8		osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
9		inass	$⊢ (\underset{˙}{⊥} (X) \cap U) \cap M = \underset{˙}{⊥} (X) \cap (U \cap M)$
10		simp11	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to K \in HL$
11		simp13	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \in C$
12		simp21	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq \underset{˙}{⊥} (Y)$
13	1 2 3 4 5 6 7 8	osumcllem3N	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (X) \cap U = Y$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (X) \cap U = Y$
15	14	ineq1d	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to (\underset{˙}{⊥} (X) \cap U) \cap M = Y \cap M$
16	9 15	eqtr3id	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (X) \cap (U \cap M) = Y \cap M$
17		simp12	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \in C$
18	3 6	psubclssatN	$⊢ (K \in HL \land X \in C) \to X \subseteq A$
19	10 17 18	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq A$
20	3 6	psubclssatN	$⊢ (K \in HL \land Y \in C) \to Y \subseteq A$
21	10 11 20	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \subseteq A$
22		simp22	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \neq \emptyset$
23	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$
24	10 19 21 23	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} Y \subseteq A$
25	3 5	polssatN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
26	10 24 25	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
27	3 5	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
28	10 26 27	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
29	8 28	eqsstrid	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to U \subseteq A$
30		simp23	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to p \in U$
31	29 30	sseldd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to p \in A$
32		simp3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \neg p \in (X \underset{˙}{+} Y)$
33	1 2 3 4 5 6 7 8	osumcllem8N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \cap M = \emptyset$
34	10 19 21 12 22 31 32 33	syl331anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \cap M = \emptyset$
35	16 34	eqtrd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (X) \cap (U \cap M) = \emptyset$
36	35	fveq2d	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap (U \cap M)) = \underset{˙}{⊥} (\emptyset)$
37	3 5	pol0N	$⊢ K \in HL \to \underset{˙}{⊥} (\emptyset) = A$
38	10 37	syl	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\emptyset) = A$
39	36 38	eqtrd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap (U \cap M)) = A$
40	1 2 3 4 5 6 7 8	osumcllem1N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \cap M = M$
41	10 19 21 30 40	syl31anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to U \cap M = M$
42	39 41	ineq12d	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap (U \cap M)) \cap (U \cap M) = A \cap M$
43	3 5 6	polsubclN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \in C$
44	10 26 43	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \in C$
45	8 44	eqeltrid	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to U \in C$
46	3 4 6	paddatclN	$⊢ (K \in HL \land X \in C \land p \in A) \to X \underset{˙}{+} \{p\} \in C$
47	10 17 31 46	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} \{p\} \in C$
48	7 47	eqeltrid	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to M \in C$
49	6	psubclinN	$⊢ (K \in HL \land U \in C \land M \in C) \to U \cap M \in C$
50	10 45 48 49	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to U \cap M \in C$
51	1 2 3 4 5 6 7 8	osumcllem2N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq U \cap M$
52	10 19 21 30 51	syl31anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq U \cap M$
53	6 5	poml6N	$⊢ ((K \in HL \land X \in C \land U \cap M \in C) \land X \subseteq U \cap M) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap (U \cap M)) \cap (U \cap M) = X$
54	10 17 50 52 53	syl31anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap (U \cap M)) \cap (U \cap M) = X$
55	31	snssd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to \{p\} \subseteq A$
56	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land \{p\} \subseteq A) \to X \underset{˙}{+} \{p\} \subseteq A$
57	10 19 55 56	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} \{p\} \subseteq A$
58	7 57	eqsstrid	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to M \subseteq A$
59		sseqin2	$⊢ M \subseteq A \leftrightarrow A \cap M = M$
60	58 59	sylib	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to A \cap M = M$
61	42 54 60	3eqtr3rd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in U) \land \neg p \in (X \underset{˙}{+} Y)) \to M = X$

Metamath Proof Explorer

Theorem osumcllem9N

Proof