cdleme0c

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 12-Jun-2012)

	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$
Assertion	cdleme0c	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to U \neq R$

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		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to K \in Lat$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to P \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
12	9 11	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
13		simp2r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to Q \in A$
14	10 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to Q \in {Base}_{K}$
16	10 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
17	8 12 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
18		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to W \in H$
19	10 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
21	10 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
22	8 17 20 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
23	6 22	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to U \underset{˙}{\leq} W$
24		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to \neg R \underset{˙}{\leq} W$
25		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg R \underset{˙}{\leq} W) \to U \neq R$
26	23 24 25	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to U \neq R$

Metamath Proof Explorer

Theorem cdleme0c

Proof