cdlemg31d

Description: Eliminate ( FP ) =/= P from cdlemg31c . TODO: Prove directly. TODO: do we need to eliminate ( FP ) =/= P ? It might be better to do this all at once at the end. See also cdlemg29 versus cdlemg28 . (Contributed by NM, 29-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)$
	cdlemg31.n	$⊢ N = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))$
Assertion	cdlemg31d	$⊢ ((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to \neg N \underset{˙}{\leq} W$

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		cdlemg31.n	$⊢ N = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))$
9		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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to \neg Q \underset{˙}{\leq} W$
10	9	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to \neg Q \underset{˙}{\leq} W$
11		simpl1	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to (K \in HL \land W \in H)$
12		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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to P \in A$
13	12	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to P \in A$
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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to Q \in A$
15	14	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to Q \in A$
16		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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to v \in A$
17	16	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to v \in A$
18		simpl31	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to F \in T$
19	1 2 3 4 5 6 7 8	cdlemg31b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
20	11 13 15 17 18 19	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
21		simpl21	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
22		simpr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to F (P) = P$
23		eqid	$⊢ 0. (K) = 0. (K)$
24	1 23 4 5 6 7	trl0	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) = P)) \to R (F) = 0. (K)$
25	11 21 18 22 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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to R (F) = 0. (K)$
26	25	oveq2d	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to Q \underset{˙}{\lor} R (F) = Q \underset{˙}{\lor} 0. (K)$
27		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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to K \in HL$
28		hlol	$⊢ K \in HL \to K \in OL$
29	27 28	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to K \in OL$
30	29	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to K \in OL$
31		eqid	$⊢ {Base}_{K} = {Base}_{K}$
32	31 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
33	15 32	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to Q \in {Base}_{K}$
34	31 2 23	olj01	$⊢ (K \in OL \land Q \in {Base}_{K}) \to Q \underset{˙}{\lor} 0. (K) = Q$
35	30 33 34	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to Q \underset{˙}{\lor} 0. (K) = Q$
36	26 35	eqtrd	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to Q \underset{˙}{\lor} R (F) = Q$
37	20 36	breqtrd	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to N \underset{˙}{\leq} Q$
38		hlatl	$⊢ K \in HL \to K \in AtLat$
39	27 38	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to K \in AtLat$
40	39	adantr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to K \in AtLat$
41		simpl33	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to N \in A$
42	1 4	atcmp	$⊢ (K \in AtLat \land N \in A \land Q \in A) \to (N \underset{˙}{\leq} Q \leftrightarrow N = Q)$
43	40 41 15 42	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to (N \underset{˙}{\leq} Q \leftrightarrow N = Q)$
44	37 43	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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to N = Q$
45	44	breq1d	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to (N \underset{˙}{\leq} W \leftrightarrow Q \underset{˙}{\leq} W)$
46	10 45	mtbird	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) = P) \to \neg N \underset{˙}{\leq} W$
47		simpl1	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to (K \in HL \land W \in H)$
48		simpl21	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
49		simpl22	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
50		simpl23	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to (v \in A \land v \underset{˙}{\leq} W)$
51		simpl31	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to F \in T$
52		simpl32	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to v \neq R (F)$
53		simpr	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to F (P) \neq P$
54		simpl33	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to N \in A$
55	1 2 3 4 5 6 7 8	cdlemg31c	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land F \in T) \land (v \neq R (F) \land F (P) \neq P \land N \in A)) \to \neg N \underset{˙}{\leq} W$
56	47 48 49 50 51 52 53 54 55	syl323anc	$⊢ (((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \land F (P) \neq P) \to \neg N \underset{˙}{\leq} W$
57	46 56	pm2.61dane	$⊢ ((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to \neg N \underset{˙}{\leq} W$

Metamath Proof Explorer

Theorem cdlemg31d

Proof