atbtwn

Description: Property of a 3rd atom R on a line P .\/ Q intersecting element X at P . (Contributed by NM, 30-Jul-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	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)$

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		simpl33	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
6		simpr	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} X$
7		simpl11	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to K \in HL$
8	7	hllatd	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to K \in Lat$
9		simpl2l	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \in A$
10	1 4	atbase	$⊢ R \in A \to R \in B$
11	9 10	syl	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \in B$
12		simpl1	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to (K \in HL \land P \in A \land Q \in A)$
13	1 3 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in B$
14	12 13	syl	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to P \underset{˙}{\lor} Q \in B$
15		simpl2r	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to X \in B$
16		eqid	$⊢ meet (K) = meet (K)$
17	1 2 16	latlem12	$⊢ (K \in Lat \land (R \in B \land P \underset{˙}{\lor} Q \in B \land X \in B)) \to ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} X) \leftrightarrow R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) meet (K) X))$
18	8 11 14 15 17	syl13anc	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} X) \leftrightarrow R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) meet (K) X))$
19	5 6 18	mpbi2and	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) meet (K) X)$
20		simpl12	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to P \in A$
21		simpl13	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to Q \in A$
22		simpl31	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X$
23		simpl32	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to \neg Q \underset{˙}{\leq} X$
24	1 2 3 16 4	2atjm	$⊢ (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{˙}{\lor} Q) meet (K) X = P$
25	7 20 21 15 22 23 24	syl132anc	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to (P \underset{˙}{\lor} Q) meet (K) X = P$
26	19 25	breqtrd	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} P$
27		hlatl	$⊢ K \in HL \to K \in AtLat$
28	7 27	syl	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to K \in AtLat$
29	2 4	atcmp	$⊢ (K \in AtLat \land R \in A \land P \in A) \to (R \underset{˙}{\leq} P \leftrightarrow R = P)$
30	28 9 20 29	syl3anc	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to (R \underset{˙}{\leq} P \leftrightarrow R = P)$
31	26 30	mpbid	$⊢ (((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))) \land R \underset{˙}{\leq} X) \to R = P$
32	31	ex	$⊢ ((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 \underset{˙}{\leq} X \to R = P)$
33	32	necon3ad	$⊢ ((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 \to \neg R \underset{˙}{\leq} X)$
34		simp31	$⊢ ((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 P \underset{˙}{\leq} X$
35		nbrne2	$⊢ (P \underset{˙}{\leq} X \land \neg R \underset{˙}{\leq} X) \to P \neq R$
36	35	necomd	$⊢ (P \underset{˙}{\leq} X \land \neg R \underset{˙}{\leq} X) \to R \neq P$
37	36	ex	$⊢ P \underset{˙}{\leq} X \to (\neg R \underset{˙}{\leq} X \to R \neq P)$
38	34 37	syl	$⊢ ((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 (\neg R \underset{˙}{\leq} X \to R \neq P)$
39	33 38	impbid	$⊢ ((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)$

Metamath Proof Explorer

Theorem atbtwn

Proof