osumcllem3N

Description: Lemma for osumclN . (Contributed by NM, 23-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	osumcllem3N	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (X) \cap U = Y$

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		incom	$⊢ \underset{˙}{⊥} (X) \cap U = U \cap \underset{˙}{⊥} (X)$
10		simp1	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to K \in HL$
11		simp3	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq \underset{˙}{⊥} (Y)$
12	3 6	psubclssatN	$⊢ (K \in HL \land Y \in C) \to Y \subseteq A$
13	12	3adant3	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq A$
14	3 5	polssatN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (Y) \subseteq A$
15	10 13 14	syl2anc	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (Y) \subseteq A$
16	11 15	sstrd	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq A$
17	3 4 5	poldmj1N	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
18	10 16 13 17	syl3anc	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)$
19		incom	$⊢ \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X)$
20	18 19	eqtrdi	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) = \underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X)$
21	20	fveq2d	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X))$
22	8 21	eqtrid	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to U = \underset{˙}{⊥} (\underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X))$
23	22	ineq1d	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to U \cap \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X)$
24	3 5	polcon2N	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (X)$
25	13 24	syld3an2	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (X)$
26	3 5	poml5N	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
27	10 16 25 26	syl3anc	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y) \cap \underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
28	5 6	psubcli2N	$⊢ (K \in HL \land Y \in C) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
29	28	3adant3	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
30	23 27 29	3eqtrd	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to U \cap \underset{˙}{⊥} (X) = Y$
31	9 30	eqtrid	$⊢ (K \in HL \land Y \in C \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (X) \cap U = Y$

Metamath Proof Explorer

Theorem osumcllem3N

Proof