osumcllem6N

Description: Lemma for osumclN . Use atom exchange hlatexch1 to swap p and q . (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	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)$

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 p \in A) \land (r \in X \land q \in Y \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to K \in HL$
10		simp12	$⊢ ((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 X \subseteq A$
11		simp13	$⊢ ((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 Y \subseteq A$
12		simp2r	$⊢ ((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 A$
13		simp31	$⊢ ((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 r \in X$
14		simp32	$⊢ ((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 q \in Y$
15	11 14	sseldd	$⊢ ((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 q \in A$
16	10 13	sseldd	$⊢ ((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 r \in A$
17	15 12 16	3jca	$⊢ ((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 (q \in A \land p \in A \land r \in A)$
18		simp2l	$⊢ ((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 X \subseteq \underset{˙}{⊥} (Y)$
19	1 2 3 4 5 6 7 8	osumcllem4N	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to q \neq r$
20	9 11 18 13 14 19	syl32anc	$⊢ ((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 q \neq r$
21	9 17 20	3jca	$⊢ ((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 (K \in HL \land (q \in A \land p \in A \land r \in A) \land q \neq r)$
22		simp33	$⊢ ((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 q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
23	1 2 3	hlatexch1	$⊢ (K \in HL \land (q \in A \land p \in A \land r \in A) \land q \neq r) \to (q \underset{˙}{\leq} (r \underset{˙}{\lor} p) \to p \underset{˙}{\leq} (r \underset{˙}{\lor} q))$
24	21 22 23	sylc	$⊢ ((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 \underset{˙}{\leq} (r \underset{˙}{\lor} q)$
25	1 2 3 4 5 6 7 8	osumcllem5N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land (r \in X \land q \in Y \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \in (X \underset{˙}{+} Y)$
26	9 10 11 12 13 14 24 25	syl313anc	$⊢ ((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)$

Metamath Proof Explorer

Theorem osumcllem6N

Proof