cdlemf

Description: Lemma F in Crawley p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013)

	Ref	Expression
Hypotheses	cdlemf.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemf.a	$⊢ A = Atoms (K)$
	cdlemf.h	$⊢ H = LHyp (K)$
	cdlemf.t	$⊢ T = LTrn (K) (W)$
	cdlemf.r	$⊢ R = trL (K) (W)$
Assertion	cdlemf	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists f \in T R (f) = U$

Proof

Step	Hyp	Ref	Expression
1		cdlemf.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemf.a	$⊢ A = Atoms (K)$
3		cdlemf.h	$⊢ H = LHyp (K)$
4		cdlemf.t	$⊢ T = LTrn (K) (W)$
5		cdlemf.r	$⊢ R = trL (K) (W)$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ meet (K) = meet (K)$
8	1 6 2 3 7	cdlemf2	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists p \in A \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)$
9		simp1l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to (K \in HL \land W \in H)$
10		simp2l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to p \in A$
11		simp3ll	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to \neg p \underset{˙}{\leq} W$
12		simp2r	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to q \in A$
13		simp3lr	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to \neg q \underset{˙}{\leq} W$
14	1 2 3 4	cdleme50ex	$⊢ ((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)) \to \exists f \in T f (p) = q$
15	9 10 11 12 13 14	syl122anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to \exists f \in T f (p) = q$
16		simp3r	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to f (p) = q$
17	16	oveq2d	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to p join (K) f (p) = p join (K) q$
18	17	oveq1d	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to (p join (K) f (p)) meet (K) W = (p join (K) q) meet (K) W$
19		simp11	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to (K \in HL \land W \in H)$
20		simp3l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to f \in T$
21		simp13l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to p \in A$
22		simp2ll	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to \neg p \underset{˙}{\leq} W$
23	1 6 7 2 3 4 5	trlval2	$⊢ ((K \in HL \land W \in H) \land f \in T \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to R (f) = (p join (K) f (p)) meet (K) W$
24	19 20 21 22 23	syl112anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to R (f) = (p join (K) f (p)) meet (K) W$
25		simp2r	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to U = (p join (K) q) meet (K) W$
26	18 24 25	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \land (f \in T \land f (p) = q)) \to R (f) = U$
27	26	3exp	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W) \land (p \in A \land q \in A)) \to (((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \to ((f \in T \land f (p) = q) \to R (f) = U))$
28	27	3expia	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to ((p \in A \land q \in A) \to (((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \to ((f \in T \land f (p) = q) \to R (f) = U)))$
29	28	3imp	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to ((f \in T \land f (p) = q) \to R (f) = U)$
30	29	expd	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to (f \in T \to (f (p) = q \to R (f) = U))$
31	30	reximdvai	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to (\exists f \in T f (p) = q \to \exists f \in T R (f) = U)$
32	15 31	mpd	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land (p \in A \land q \in A) \land ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W)) \to \exists f \in T R (f) = U$
33	32	3exp	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to ((p \in A \land q \in A) \to (((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \to \exists f \in T R (f) = U))$
34	33	rexlimdvv	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to (\exists p \in A \exists q \in A ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land U = (p join (K) q) meet (K) W) \to \exists f \in T R (f) = U)$
35	8 34	mpd	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists f \in T R (f) = U$

Metamath Proof Explorer

Theorem cdlemf

Proof