trlat

Description: If an atom differs from its translation, the trace is an atom. Equation above Lemma C in Crawley p. 112. (Contributed by NM, 23-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		trlat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlat.a	$⊢ A = Atoms (K)$
3		trlat.h	$⊢ H = LHyp (K)$
4		trlat.t	$⊢ T = LTrn (K) (W)$
5		trlat.r	$⊢ R = trL (K) (W)$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to (K \in HL \land W \in H)$
7		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to F \in T$
8		simp2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		eqid	$⊢ join (K) = join (K)$
10		eqid	$⊢ meet (K) = meet (K)$
11	1 9 10 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$
12	6 7 8 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) = (P join (K) F (P)) meet (K) W$
13		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to P \in A$
14	1 2 3 4	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
15	6 7 13 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to F (P) \in A$
16		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to F (P) \neq P$
17	16	necomd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to P \neq F (P)$
18	1 9 10 2 3	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F (P) \in A \land P \neq F (P))) \to (P join (K) F (P)) meet (K) W \in A$
19	6 8 15 17 18	syl112anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to (P join (K) F (P)) meet (K) W \in A$
20	12 19	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$

Metamath Proof Explorer

Theorem trlat

Proof