cdleme3e

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme1.a	$⊢ A = Atoms (K)$
	cdleme1.h	$⊢ H = LHyp (K)$
	cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	cdleme3.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
Assertion	cdleme3e	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to V \in A$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8		cdleme3.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
9		simpl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (K \in HL \land W \in H)$
10		simpr1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		simpr3l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \in A$
12		hllat	$⊢ K \in HL \to K \in Lat$
13	12	ad2antrr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to K \in Lat$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
16	11 15	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \in {Base}_{K}$
17		simpr1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \in A$
18	14 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
19	17 18	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \in {Base}_{K}$
20		simpr2	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in A$
21	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
22	20 21	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in {Base}_{K}$
23		simpr3r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
24	14 1 2	latnlej1l	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq P$
25	13 16 19 22 23 24	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \neq P$
26	25	necomd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq R$
27	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land P \neq R)) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in A$
28	9 10 11 26 27	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in A$
29	8 28	eqeltrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to V \in A$

Metamath Proof Explorer

Theorem cdleme3e

Proof