cdleme0b

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 13-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	cdleme0b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to U \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		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to K \in Lat$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \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 \neg P \underset{˙}{\leq} W) \land Q \in A) \to P \in {Base}_{K}$
13	10 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
14	13	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to Q \in {Base}_{K}$
15	10 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
16	8 12 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
17		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to W \in H$
18	10 5	lhpbase	$⊢ W \in H \to W \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) \to W \in {Base}_{K}$
20	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$
21	8 16 19 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
22	6 21	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to U \underset{˙}{\leq} W$
23		simp2r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to \neg P \underset{˙}{\leq} W$
24		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to U \neq P$
25	22 23 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to U \neq P$

Metamath Proof Explorer

Theorem cdleme0b

Proof