cdleme0fN

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 14-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme0.a	$⊢ A = Atoms (K)$
	cdleme0.h	$⊢ H = LHyp (K)$
	cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme0c.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
Assertion	cdleme0fN	$⊢ ((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)) \to V \neq P$

Proof

Step	Hyp	Ref	Expression
1		cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme0.a	$⊢ A = Atoms (K)$
5		cdleme0.h	$⊢ H = LHyp (K)$
6		cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme0c.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
8		simp1l	$⊢ ((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)) \to K \in HL$
9	8	hllatd	$⊢ ((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)) \to K \in Lat$
10		simp2l	$⊢ ((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)) \to P \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	10 12	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)) \to P \in {Base}_{K}$
14		simp3r	$⊢ ((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)) \to R \in A$
15	11 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
16	14 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)) \to R \in {Base}_{K}$
17	11 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \underset{˙}{\lor} R \in {Base}_{K}$
18	9 13 16 17	syl3anc	$⊢ ((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)) \to P \underset{˙}{\lor} R \in {Base}_{K}$
19		simp1r	$⊢ ((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)) \to W \in H$
20	11 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
21	19 20	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)) \to W \in {Base}_{K}$
22	11 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} W$
23	9 18 21 22	syl3anc	$⊢ ((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)) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} W$
24	7 23	eqbrtrid	$⊢ ((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)) \to V \underset{˙}{\leq} W$
25		simp2r	$⊢ ((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)) \to \neg P \underset{˙}{\leq} W$
26		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to V \neq P$
27	24 25 26	syl2anc	$⊢ ((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)) \to V \neq P$

Metamath Proof Explorer

Theorem cdleme0fN

Proof