osumcllem2N

Description: Lemma for osumclN . (Contributed by NM, 25-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	osumcllem2N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq U \cap M$

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		simpl1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to K \in HL$
10		simpl2	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq A$
11		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to p \in U$
12	11	snssd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \{p\} \subseteq U$
13	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$
14	13	adantr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \underset{˙}{+} Y \subseteq A$
15	3 5	polssatN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
16	9 14 15	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
17	3 5	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
18	9 16 17	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
19	8 18	eqsstrid	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \subseteq A$
20	12 19	sstrd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \{p\} \subseteq A$
21	3 4	sspadd1	$⊢ (K \in HL \land X \subseteq A \land \{p\} \subseteq A) \to X \subseteq X \underset{˙}{+} \{p\}$
22	9 10 20 21	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq X \underset{˙}{+} \{p\}$
23	22 7	sseqtrrdi	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq M$
24	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$
25	23 24	sseqtrrd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq U \cap M$

Metamath Proof Explorer

Theorem osumcllem2N

Proof