osumcllem7N

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	osumcllem7N	$⊢ ((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 q \in (Y \cap M)) \to p \in (X \underset{˙}{+} 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		simp11	$⊢ ((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 q \in (Y \cap M)) \to K \in HL$
10	9	hllatd	$⊢ ((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 q \in (Y \cap M)) \to K \in Lat$
11		simp12	$⊢ ((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 q \in (Y \cap M)) \to X \subseteq A$
12		simp23	$⊢ ((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 q \in (Y \cap M)) \to p \in A$
13		simp22	$⊢ ((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 q \in (Y \cap M)) \to X \neq \emptyset$
14		inss2	$⊢ Y \cap M \subseteq M$
15	14	sseli	$⊢ q \in (Y \cap M) \to q \in M$
16	15	3ad2ant3	$⊢ ((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 q \in (Y \cap M)) \to q \in M$
17	16 7	eleqtrdi	$⊢ ((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 q \in (Y \cap M)) \to q \in (X \underset{˙}{+} \{p\})$
18	1 2 3 4	elpaddatiN	$⊢ ((K \in Lat \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (X \underset{˙}{+} \{p\}))) \to \exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
19	10 11 12 13 17 18	syl32anc	$⊢ ((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 q \in (Y \cap M)) \to \exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
20		simp11	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to (K \in HL \land X \subseteq A \land Y \subseteq A)$
21		simp121	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to X \subseteq \underset{˙}{⊥} (Y)$
22		simp123	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in A$
23		simp2	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to r \in X$
24		inss1	$⊢ Y \cap M \subseteq Y$
25		simp13	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to q \in (Y \cap M)$
26	24 25	sselid	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to q \in Y$
27		simp3	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
28	1 2 3 4 5 6 7 8	osumcllem6N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land p \in A) \land (r \in X \land q \in Y \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to p \in (X \underset{˙}{+} Y)$
29	20 21 22 23 26 27 28	syl123anc	$⊢ (((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 q \in (Y \cap M)) \land r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in (X \underset{˙}{+} Y)$
30	29	rexlimdv3a	$⊢ ((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 q \in (Y \cap M)) \to (\exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p) \to p \in (X \underset{˙}{+} Y))$
31	19 30	mpd	$⊢ ((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 q \in (Y \cap M)) \to p \in (X \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem osumcllem7N

Proof