cdleme11h

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-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$
	cdleme11.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
Assertion	cdleme11h	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq Q$

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		cdleme11.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10		simp1	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
11		simp21l	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
12		simp23	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
13		simp22l	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
14		simp22r	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Q \underset{˙}{\leq} W$
15	1 2 3 4 5 7	cdleme0c	$⊢ ((K \in HL \land W \in H) \land (P \in A \land S \in A) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to C \neq Q$
16	10 11 12 13 14 15	syl122anc	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \neq Q$
17	16	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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \neq C$
18		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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
19		simp21	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
20		simp3r	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
21	1 2 3 4	cdleme00a	$⊢ (K \in HL \land (P \in A \land Q \in A \land S \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
22	18 11 13 12 20 21	syl131anc	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \neq P$
23	22	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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq S$
24	1 2 3 4 5 7	cdleme9a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land P \neq S)) \to C \in A$
25	10 19 12 23 24	syl112anc	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \in A$
26	2 4	lnnat	$⊢ (K \in HL \land Q \in A \land C \in A) \to (Q \neq C \leftrightarrow \neg Q \underset{˙}{\lor} C \in A)$
27	18 13 25 26	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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \neq C \leftrightarrow \neg Q \underset{˙}{\lor} C \in A)$
28	17 27	mpbid	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Q \underset{˙}{\lor} C \in A$
29	2 4	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
30	18 13 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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\lor} Q = Q$
31	30 13	eqeltrd	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\lor} Q \in A$
32		oveq2	$⊢ F = Q \to Q \underset{˙}{\lor} F = Q \underset{˙}{\lor} Q$
33	32	eleq1d	$⊢ F = Q \to (Q \underset{˙}{\lor} F \in A \leftrightarrow Q \underset{˙}{\lor} Q \in A)$
34	31 33	syl5ibrcom	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F = Q \to Q \underset{˙}{\lor} F \in A)$
35		simp22	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
36		simp3l	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq Q$
37	1 2 3 4 5 6 7 6 9	cdleme11g	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} F = Q \underset{˙}{\lor} C$
38	10 11 35 12 36 37	syl131anc	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\lor} F = Q \underset{˙}{\lor} C$
39	38	eleq1d	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \underset{˙}{\lor} F \in A \leftrightarrow Q \underset{˙}{\lor} C \in A)$
40	34 39	sylibd	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F = Q \to Q \underset{˙}{\lor} C \in A)$
41	40	necon3bd	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg Q \underset{˙}{\lor} C \in A \to F \neq Q)$
42	28 41	mpd	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq Q$

Metamath Proof Explorer

Theorem cdleme11h

Proof