osumcllem1N

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	osumcllem1N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \cap M = 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	3 4	sspadd1	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \subseteq X \underset{˙}{+} Y$
10	9	adantr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq X \underset{˙}{+} Y$
11		simpl1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to K \in HL$
12	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$
13	12	adantr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \underset{˙}{+} Y \subseteq A$
14	3 5	2polssN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A) \to X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
15	11 13 14	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
16	15 8	sseqtrrdi	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \underset{˙}{+} Y \subseteq U$
17	10 16	sstrd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq U$
18		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to p \in U$
19	18	snssd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \{p\} \subseteq U$
20		simpl2	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \subseteq A$
21	3 5	polssatN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
22	11 13 21	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A$
23	3 5	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
24	11 22 23	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq A$
25	8 24	eqsstrid	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \subseteq A$
26	19 25	sstrd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \{p\} \subseteq A$
27		eqid	$⊢ PSubSp (K) = PSubSp (K)$
28	3 27 5	polsubN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \in PSubSp (K)$
29	11 22 28	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \in PSubSp (K)$
30	8 29	eqeltrid	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \in PSubSp (K)$
31	3 27 4	paddss	$⊢ (K \in HL \land (X \subseteq A \land \{p\} \subseteq A \land U \in PSubSp (K))) \to ((X \subseteq U \land \{p\} \subseteq U) \leftrightarrow X \underset{˙}{+} \{p\} \subseteq U)$
32	11 20 26 30 31	syl13anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to ((X \subseteq U \land \{p\} \subseteq U) \leftrightarrow X \underset{˙}{+} \{p\} \subseteq U)$
33	17 19 32	mpbi2and	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to X \underset{˙}{+} \{p\} \subseteq U$
34	7 33	eqsstrid	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to M \subseteq U$
35		sseqin2	$⊢ M \subseteq U \leftrightarrow U \cap M = M$
36	34 35	sylib	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in U) \to U \cap M = M$

Metamath Proof Explorer

Theorem osumcllem1N

Proof