cdleme11e

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

	Ref	Expression
Hypotheses	cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme11.a	$⊢ A = Atoms (K)$
	cdleme11.h	$⊢ H = LHyp (K)$
	cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme11.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme11.d	$⊢ D = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
Assertion	cdleme11e	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to C \neq D$

Proof

Step	Hyp	Ref	Expression
1		cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme11.a	$⊢ A = Atoms (K)$
5		cdleme11.h	$⊢ H = LHyp (K)$
6		cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme11.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
8		cdleme11.d	$⊢ D = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
9		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (K \in HL \land W \in H)$
10		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
12		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
13		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
14	13	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in Lat$
15		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
18	15 17	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in {Base}_{K}$
19		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
20	16 4	atbase	$⊢ S \in A \to S \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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in {Base}_{K}$
22	16 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
23	11 22	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in {Base}_{K}$
24		simp1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)$
25		simp2	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q)$
26		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
27		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
28	1 2 3 4 5 6	cdleme11c	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
29	24 25 26 27 28	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
30	16 1 2	latnlej1r	$⊢ (K \in Lat \land (P \in {Base}_{K} \land S \in {Base}_{K} \land T \in {Base}_{K}) \land \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to P \neq T$
31	14 18 21 23 29 30	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \neq T$
32		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
33	1 2 4	hlatcon2	$⊢ (K \in HL \land (S \in A \land T \in A \land P \in A) \land (S \neq T \land \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} T)$
34	13 19 11 15 32 29 33	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} T)$
35	1 2 3 4 5 8 7	cdleme0e	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land T \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} T))) \to D \neq C$
36	9 10 11 12 31 34 35	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \neq C$
37	36	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to C \neq D$

Metamath Proof Explorer

Theorem cdleme11e

Proof