atbtwnex

Description: Given atoms P in X and Q not in X , there exists an atom r not in X such that the line Q .\/ r intersects X at P . (Contributed by NM, 1-Aug-2012)

	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	atbtwnex	$⊢ ((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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$

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		simp1l1	$⊢ (((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$
23		simp1l2	$⊢ (((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 \in A$
24		simp1l3	$⊢ (((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 Q \in A$
25	2 3 4	hlatexch2	$⊢ (K \in HL \land (r \in A \land P \in A \land Q \in A) \land r \neq Q) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (r \underset{˙}{\lor} Q))$
26	22 14 23 24 11 25	syl131anc	$⊢ (((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) \to P \underset{˙}{\leq} (r \underset{˙}{\lor} Q))$
27	18 26	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)) \land r \in A \land (r \neq P \land r \neq Q \land r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\leq} (r \underset{˙}{\lor} Q)$
28	3 4	hlatjcom	$⊢ (K \in HL \land Q \in A \land r \in A) \to Q \underset{˙}{\lor} r = r \underset{˙}{\lor} Q$
29	22 24 14 28	syl3anc	$⊢ (((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 Q \underset{˙}{\lor} r = r \underset{˙}{\lor} Q$
30	27 29	breqtrrd	$⊢ (((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} (Q \underset{˙}{\lor} r)$
31	11 21 30	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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
32	31	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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
33	32	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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
34	10 33	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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$

Metamath Proof Explorer

Theorem atbtwnex

Proof