cdlemg18b

Description: Lemma for cdlemg18c . TODO: fix comment. (Contributed by NM, 15-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
	cdlemg18b.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdlemg18b	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to \neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		cdlemg18b.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
9		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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q$
10		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to K \in HL$
12		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to W \in H$
13		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
14		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to Q \in A$
15		simp3l1	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \neq Q$
16	1 2 3 4 5 8	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$
17	11 12 13 14 15 16	syl212anc	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to U \in A$
18		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to (K \in HL \land W \in H)$
19		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F \in T$
20	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
21	18 19 14 20	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (Q) \in A$
22	1 2 4	hlatlej1	$⊢ (K \in HL \land U \in A \land F (Q) \in A) \to U \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
23	11 17 21 22	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to U \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
24	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to K \in Lat$
25		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \in A$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27	26 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
28	25 27	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \in {Base}_{K}$
29	26 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
30	17 29	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to U \in {Base}_{K}$
31	26 2 4	hlatjcl	$⊢ (K \in HL \land U \in A \land F (Q) \in A) \to U \underset{˙}{\lor} F (Q) \in {Base}_{K}$
32	11 17 21 31	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to U \underset{˙}{\lor} F (Q) \in {Base}_{K}$
33	26 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land U \in {Base}_{K} \land U \underset{˙}{\lor} F (Q) \in {Base}_{K})) \to ((P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \land U \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))$
34	24 28 30 32 33	syl13anc	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to ((P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \land U \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))$
35	10 23 34	mpbi2and	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to (P \underset{˙}{\lor} U) \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$
36	1 2 3 4 5 8	cdleme0cp	$⊢ ((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} U = P \underset{˙}{\lor} Q$
37	11 12 13 14 36	syl22anc	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
38		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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
39	5 6 1 2 4 3 8	cdlemg2kq	$⊢ ((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 F \in T) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} U$
40	18 13 38 19 39	syl121anc	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} U$
41	2 4	hlatjcom	$⊢ (K \in HL \land F (Q) \in A \land U \in A) \to F (Q) \underset{˙}{\lor} U = U \underset{˙}{\lor} F (Q)$
42	11 21 17 41	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (Q) \underset{˙}{\lor} U = U \underset{˙}{\lor} F (Q)$
43	40 42	eqtr2d	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to U \underset{˙}{\lor} F (Q) = F (P) \underset{˙}{\lor} F (Q)$
44	35 37 43	3brtr3d	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} F (Q))$
45	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
46	18 19 25 45	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (P) \in A$
47	1 2 4	ps-1	$⊢ (K \in HL \land (P \in A \land Q \in A \land P \neq Q) \land (F (P) \in A \land F (Q) \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} F (Q)) \leftrightarrow P \underset{˙}{\lor} Q = F (P) \underset{˙}{\lor} F (Q))$
48	11 25 14 15 46 21 47	syl132anc	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} F (Q)) \leftrightarrow P \underset{˙}{\lor} Q = F (P) \underset{˙}{\lor} F (Q))$
49	44 48	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to P \underset{˙}{\lor} Q = F (P) \underset{˙}{\lor} F (Q)$
50	2 4	hlatjcom	$⊢ (K \in HL \land F (P) \in A \land F (Q) \in A) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
51	11 46 21 50	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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
52	49 51	eqtr2d	$⊢ ((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 F \in T) \land ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q$
53	52	3exp	$⊢ (K \in HL \land W \in H) \to (((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land F \in T) \to (((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q))$
54	53	exp4a	$⊢ (K \in HL \land W \in H) \to (((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land F \in T) \to ((P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q) \to (P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q)))$
55	54	3imp	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q)$
56	55	necon3ad	$⊢ ((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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q \to \neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q)))$
57	9 56	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 F \in T) \land (P \neq Q \land F (P) \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to \neg P \underset{˙}{\leq} (U \underset{˙}{\lor} F (Q))$

Metamath Proof Explorer

Theorem cdlemg18b

Proof