cdleme21c

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 28-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme21.a	$⊢ A = Atoms (K)$
	cdleme21.h	$⊢ H = LHyp (K)$
	cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme21c	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme21.a	$⊢ A = Atoms (K)$
5		cdleme21.h	$⊢ H = LHyp (K)$
6		cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp23	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
8		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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in HL$
9		hlcvl	$⊢ K \in HL \to K \in CvLat$
10	8 9	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in CvLat$
11		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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \in A$
13		simp3l	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \in A$
14		simp13	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to Q \in A$
15	1 2 4	atnlej1	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
16	15	necomd	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq S$
17	8 12 11 14 7 16	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \neq S$
18		simp3r	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} z = S \underset{˙}{\lor} z$
19	4 2	cvlsupr7	$⊢ (K \in CvLat \land (P \in A \land S \in A \land z \in A) \land (P \neq S \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} S = z \underset{˙}{\lor} S$
20	10 11 12 13 17 18 19	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} S = z \underset{˙}{\lor} S$
21	2 4	hlatjcom	$⊢ (K \in HL \land z \in A \land S \in A) \to z \underset{˙}{\lor} S = S \underset{˙}{\lor} z$
22	8 13 12 21	syl3anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \underset{˙}{\lor} S = S \underset{˙}{\lor} z$
23	20 22	eqtrd	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} S = S \underset{˙}{\lor} z$
24	23	breq2d	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} S) \leftrightarrow U \underset{˙}{\leq} (S \underset{˙}{\lor} z))$
25		simp11r	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to W \in H$
26		simp12r	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg P \underset{˙}{\leq} W$
27		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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \neq Q$
28	1 2 3 4 5 6	cdleme0a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
29	8 25 11 26 14 27 28	syl222anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \in A$
30	8	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in Lat$
31		eqid	$⊢ {Base}_{K} = {Base}_{K}$
32	31 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
33	8 11 14 32	syl3anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
34	31 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
35	25 34	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to W \in {Base}_{K}$
36	31 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$
37	30 33 35 36	syl3anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
38	6 37	eqbrtrid	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \underset{˙}{\leq} W$
39		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to U \neq P$
40	38 26 39	syl2anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \neq P$
41	1 2 4	cvlatexch1	$⊢ (K \in CvLat \land (U \in A \land S \in A \land P \in A) \land U \neq P) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
42	10 29 12 11 40 41	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
43	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
44	8 11 14 43	syl3anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
45	1 2 3 4 5 6	cdlemeulpq	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A)) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
46	8 25 11 14 45	syl22anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
47	31 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
48	11 47	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \in {Base}_{K}$
49	31 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
50	29 49	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \in {Base}_{K}$
51	31 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land U \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
52	30 48 50 33 51	syl13anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
53	44 46 52	mpbi2and	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (P \underset{˙}{\lor} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
54	31 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
55	12 54	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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \in {Base}_{K}$
56	31 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
57	8 11 29 56	syl3anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} U \in {Base}_{K}$
58	31 1	lattr	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \underset{˙}{\lor} U \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land (P \underset{˙}{\lor} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
59	30 55 57 33 58	syl13anc	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land (P \underset{˙}{\lor} U) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
60	53 59	mpan2d	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
61	42 60	syld	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
62	24 61	sylbird	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (S \underset{˙}{\lor} z) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
63	7 62	mtod	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem cdleme21c

Proof