cdleme19c

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, 1st line. D , F represent s_2, f(s). We prove f(s) =/= s_2. (Contributed by NM, 13-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme19.a	$⊢ A = Atoms (K)$
	cdleme19.h	$⊢ H = LHyp (K)$
	cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
Assertion	cdleme19c	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq D$

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme19.a	$⊢ A = Atoms (K)$
5		cdleme19.h	$⊢ H = LHyp (K)$
6		cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10		cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
11		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
12	11	hllatd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
13		simp31	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
14		simp23l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
17	11 13 14 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
18		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in H$
19	15 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 \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
21	15 1 3	latmle2	$⊢ (K \in Lat \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} W$
22	12 17 20 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} W$
23	9 22	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to D \underset{˙}{\leq} W$
24		simp32	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq Q$
25		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26	24 25	jca	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
27	1 2 3 4 5 6 7	cdleme3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg F \underset{˙}{\leq} W$
28	26 27	syld3an3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg F \underset{˙}{\leq} W$
29		nbrne2	$⊢ (D \underset{˙}{\leq} W \land \neg F \underset{˙}{\leq} W) \to D \neq F$
30	23 28 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to D \neq F$
31	30	necomd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq D$

Metamath Proof Explorer

Theorem cdleme19c

Proof