pexmidlem3N

Description: Lemma for pexmidN . Use atom exchange hlatexch1 to swap p and q . (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pexmidlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	pexmidlem.a	$⊢ A = Atoms (K)$
	pexmidlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pexmidlem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	pexmidlem.m	$⊢ M = X \underset{˙}{+} \{p\}$
Assertion	pexmidlem3N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		pexmidlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pexmidlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pexmidlem.a	$⊢ A = Atoms (K)$
4		pexmidlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		pexmidlem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		pexmidlem.m	$⊢ M = X \underset{˙}{+} \{p\}$
7		simp1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to (K \in HL \land X \subseteq A \land p \in A)$
8		simp2l	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to r \in X$
9		simp2r	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to q \in \underset{˙}{⊥} (X)$
10		simpl1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to K \in HL$
11		simpl2	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to X \subseteq A$
12	3 5	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
13	10 11 12	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to \underset{˙}{⊥} (X) \subseteq A$
14		simprr	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \in \underset{˙}{⊥} (X)$
15	13 14	sseldd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \in A$
16		simpl3	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to p \in A$
17		simprl	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to r \in X$
18	11 17	sseldd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to r \in A$
19	1 2 3 4 5 6	pexmidlem1N	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \neq r$
20	19	3adantl3	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \neq r$
21	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))$
22	10 15 16 18 20 21	syl131anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to (q \underset{˙}{\leq} (r \underset{˙}{\lor} p) \to p \underset{˙}{\leq} (r \underset{˙}{\lor} q))$
23	22	3impia	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \underset{˙}{\leq} (r \underset{˙}{\lor} q)$
24	1 2 3 4 5 6	pexmidlem2N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
25	7 8 9 23 24	syl13anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem pexmidlem3N

Proof