exatleN

Description: A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in Crawley p. 112. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		atomle.b	$⊢ B = {Base}_{K}$
2		atomle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atomle.j	$⊢ \underset{˙}{\lor} = join (K)$
4		atomle.a	$⊢ A = Atoms (K)$
5		simpl32	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P) \to \neg Q \underset{˙}{\leq} X$
6		simp11l	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to K \in HL$
7	6	hllatd	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to K \in Lat$
8		simp122	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to Q \in A$
9	1 4	atbase	$⊢ Q \in A \to Q \in B$
10	8 9	syl	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to Q \in B$
11		simp121	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to P \in A$
12	1 4	atbase	$⊢ P \in A \to P \in B$
13	11 12	syl	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to P \in B$
14		simp123	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to R \in A$
15	1 4	atbase	$⊢ R \in A \to R \in B$
16	14 15	syl	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to R \in B$
17	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R \in B) \to P \underset{˙}{\lor} R \in B$
18	7 13 16 17	syl3anc	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to P \underset{˙}{\lor} R \in B$
19		simp11r	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to X \in B$
20	14 8 11	3jca	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to (R \in A \land Q \in A \land P \in A)$
21		simp2	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to R \neq P$
22	6 20 21	3jca	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to (K \in HL \land (R \in A \land Q \in A \land P \in A) \land R \neq P)$
23		simp133	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
24	2 3 4	hlatexch1	$⊢ (K \in HL \land (R \in A \land Q \in A \land P \in A) \land R \neq P) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
25	22 23 24	sylc	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
26		simp131	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X$
27		simp3	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to R \underset{˙}{\leq} X$
28	1 2 3	latjle12	$⊢ (K \in Lat \land (P \in B \land R \in B \land X \in B)) \to ((P \underset{˙}{\leq} X \land R \underset{˙}{\leq} X) \leftrightarrow (P \underset{˙}{\lor} R) \underset{˙}{\leq} X)$
29	7 13 16 19 28	syl13anc	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to ((P \underset{˙}{\leq} X \land R \underset{˙}{\leq} X) \leftrightarrow (P \underset{˙}{\lor} R) \underset{˙}{\leq} X)$
30	26 27 29	mpbi2and	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to (P \underset{˙}{\lor} R) \underset{˙}{\leq} X$
31	1 2 7 10 18 19 25 30	lattrd	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P \land R \underset{˙}{\leq} X) \to Q \underset{˙}{\leq} X$
32	31	3expia	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P) \to (R \underset{˙}{\leq} X \to Q \underset{˙}{\leq} X)$
33	5 32	mtod	$⊢ (((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land R \neq P) \to \neg R \underset{˙}{\leq} X$
34	33	ex	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \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)$
35	34	necon4ad	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \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)$
36		simp31	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\leq} X$
37		breq1	$⊢ R = P \to (R \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\leq} X)$
38	36 37	syl5ibrcom	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R = P \to R \underset{˙}{\leq} X)$
39	35 38	impbid	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} X \leftrightarrow R = P)$

Metamath Proof Explorer

Theorem exatleN

Proof