cdleme50ltrn

Description: Part of proof of Lemma E in Crawley p. 113. F is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013)

	Ref	Expression
Hypotheses	cdlemef50.b	$⊢ B = {Base}_{K}$
	cdlemef50.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemef50.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemef50.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemef50.a	$⊢ A = Atoms (K)$
	cdlemef50.h	$⊢ H = LHyp (K)$
	cdlemef50.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdlemef50.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs50.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemef50.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
	cdleme50ltrn.t	$⊢ T = LTrn (K) (W)$
Assertion	cdleme50ltrn	$⊢ ((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 F \in T$

Proof

Step	Hyp	Ref	Expression
1		cdlemef50.b	$⊢ B = {Base}_{K}$
2		cdlemef50.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemef50.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemef50.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemef50.a	$⊢ A = Atoms (K)$
6		cdlemef50.h	$⊢ H = LHyp (K)$
7		cdlemef50.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdlemef50.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdlemefs50.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemef50.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
11		cdleme50ltrn.t	$⊢ T = LTrn (K) (W)$
12		eqid	$⊢ LDil (K) (W) = LDil (K) (W)$
13	1 2 3 4 5 6 7 8 9 10 12	cdleme50ldil	$⊢ ((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 F \in LDil (K) (W)$
14		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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to ((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))$
15		simp2l	$⊢ (((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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to d \in A$
16		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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to \neg d \underset{˙}{\leq} W$
17	1 2 3 4 5 6 7 8 9 10	cdleme50trn123	$⊢ (((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 (d \in A \land \neg d \underset{˙}{\leq} W)) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = U$
18	14 15 16 17	syl12anc	$⊢ (((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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = U$
19		simp2r	$⊢ (((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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to e \in A$
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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to \neg e \underset{˙}{\leq} W$
21	1 2 3 4 5 6 7 8 9 10	cdleme50trn123	$⊢ (((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 (e \in A \land \neg e \underset{˙}{\leq} W)) \to (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W = U$
22	14 19 20 21	syl12anc	$⊢ (((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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W = U$
23	18 22	eqtr4d	$⊢ (((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 (d \in A \land e \in A) \land (\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W)) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W$
24	23	3exp	$⊢ ((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 ((d \in A \land e \in A) \to ((\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W))$
25	24	ralrimivv	$⊢ ((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 \forall d \in A \forall e \in A ((\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W)$
26	2 3 4 5 6 12 11	isltrn	$⊢ (K \in HL \land W \in H) \to (F \in T \leftrightarrow (F \in LDil (K) (W) \land \forall d \in A \forall e \in A ((\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W)))$
27	26	3ad2ant1	$⊢ ((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 (F \in T \leftrightarrow (F \in LDil (K) (W) \land \forall d \in A \forall e \in A ((\neg d \underset{˙}{\leq} W \land \neg e \underset{˙}{\leq} W) \to (d \underset{˙}{\lor} F (d)) \underset{˙}{\land} W = (e \underset{˙}{\lor} F (e)) \underset{˙}{\land} W)))$
28	13 25 27	mpbir2and	$⊢ ((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 F \in T$

Metamath Proof Explorer

Theorem cdleme50ltrn

Proof