cdlema2N

Description: A condition for required for proof of Lemma A in Crawley p. 112. (Contributed by NM, 9-May-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlema2.b	$⊢ B = {Base}_{K}$
	cdlema2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlema2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlema2.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlema2.z	$⊢ \underset{˙}{0} = 0. (K)$
	cdlema2.a	$⊢ A = Atoms (K)$
Assertion	cdlema2N	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to R \underset{˙}{\land} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		cdlema2.b	$⊢ B = {Base}_{K}$
2		cdlema2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlema2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlema2.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlema2.z	$⊢ \underset{˙}{0} = 0. (K)$
6		cdlema2.a	$⊢ A = Atoms (K)$
7		simp3ll	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to R \neq P$
8		simp3rl	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to P \underset{˙}{\leq} X$
9		simp3rr	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to \neg Q \underset{˙}{\leq} X$
10		simp3lr	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
11	8 9 10	3jca	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
12	1 2 3 6	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)$
13	11 12	syld3an3	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to (R \underset{˙}{\leq} X \leftrightarrow R = P)$
14	13	necon3bbid	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to (\neg R \underset{˙}{\leq} X \leftrightarrow R \neq P)$
15	7 14	mpbird	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to \neg R \underset{˙}{\leq} X$
16		simp1l	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to K \in HL$
17		hlatl	$⊢ K \in HL \to K \in AtLat$
18	16 17	syl	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to K \in AtLat$
19		simp23	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to R \in A$
20		simp1r	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to X \in B$
21	1 2 4 5 6	atnle	$⊢ (K \in AtLat \land R \in A \land X \in B) \to (\neg R \underset{˙}{\leq} X \leftrightarrow R \underset{˙}{\land} X = \underset{˙}{0})$
22	18 19 20 21	syl3anc	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to (\neg R \underset{˙}{\leq} X \leftrightarrow R \underset{˙}{\land} X = \underset{˙}{0})$
23	15 22	mpbid	$⊢ ((K \in HL \land X \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X))) \to R \underset{˙}{\land} X = \underset{˙}{0}$

Metamath Proof Explorer

Theorem cdlema2N

Proof