atbtwnexOLDN

Description: There exists a 3rd atom r on a line P .\/ Q intersecting element X at P , such that r is different from Q and not in X . (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atbtwn.b	$⊢ B = {Base}_{K}$
	atbtwn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atbtwn.j	$⊢ \underset{˙}{\lor} = join (K)$
	atbtwn.a	$⊢ A = Atoms (K)$
Assertion	atbtwnexOLDN	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists r \in A (r \neq Q \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Proof

Step	Hyp	Ref	Expression
1		atbtwn.b	$⊢ B = {Base}_{K}$
2		atbtwn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atbtwn.j	$⊢ \underset{˙}{\lor} = join (K)$
4		atbtwn.a	$⊢ A = Atoms (K)$
5		simpr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} X$
6		simpr3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \neg Q \underset{˙}{\leq} X$
7		nbrne2	$⊢ (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X) \to P \neq Q$
8	5 6 7	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \neq Q$
9	2 3 4	hlsupr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to \exists r \in A (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
10	8 9	syldan	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists r \in A (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
11		simp32	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to r \neq Q$
12		simp31	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to r \neq P$
13		simp1l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land P \in A \land Q \in A)$
14		simp2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to r \in A$
15		simp1r1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to X \in B$
16		simp1r2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\leq} X$
17		simp1r3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Q \underset{˙}{\leq} X$
18		simp33	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
19	1 2 3 4	atbtwn	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (r \in A \land X \in B) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (r \neq P \leftrightarrow \neg r \underset{˙}{\leq} X)$
20	13 14 15 16 17 18 19	syl123anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (r \neq P \leftrightarrow \neg r \underset{˙}{\leq} X)$
21	12 20	mpbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg r \underset{˙}{\leq} X$
22	11 21 18	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (r \neq Q \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
23	22	3exp	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (r \in A \to ((r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (r \neq Q \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))))$
24	23	reximdvai	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (\exists r \in A (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \exists r \in A (r \neq Q \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
25	10 24	mpd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists r \in A (r \neq Q \land \neg r \underset{˙}{\leq} X \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem atbtwnexOLDN

Proof