trl0

Description: If an atom not under the fiducial co-atom W equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012)

	Ref	Expression
Hypotheses	trl0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	trl0.z	$⊢ \underset{˙}{0} = 0. (K)$
	trl0.a	$⊢ A = Atoms (K)$
	trl0.h	$⊢ H = LHyp (K)$
	trl0.t	$⊢ T = LTrn (K) (W)$
	trl0.r	$⊢ R = trL (K) (W)$
Assertion	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) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		trl0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trl0.z	$⊢ \underset{˙}{0} = 0. (K)$
3		trl0.a	$⊢ A = Atoms (K)$
4		trl0.h	$⊢ H = LHyp (K)$
5		trl0.t	$⊢ T = LTrn (K) (W)$
6		trl0.r	$⊢ R = trL (K) (W)$
7		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) = P)) \to (K \in HL \land W \in H)$
8		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) = P)) \to F \in T$
9		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) = P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		eqid	$⊢ join (K) = join (K)$
11		eqid	$⊢ meet (K) = meet (K)$
12	1 10 11 3 4 5 6	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$
13	7 8 9 12	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) = P)) \to R (F) = (P join (K) F (P)) meet (K) W$
14		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) = P)) \to F (P) = P$
15	14	oveq2d	$⊢ ((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 P join (K) F (P) = P join (K) P$
16		simp1l	$⊢ ((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 K \in HL$
17		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) = P)) \to P \in A$
18	10 3	hlatjidm	$⊢ (K \in HL \land P \in A) \to P join (K) P = P$
19	16 17 18	syl2anc	$⊢ ((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 P join (K) P = P$
20	15 19	eqtrd	$⊢ ((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 P join (K) F (P) = P$
21	20	oveq1d	$⊢ ((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 (P join (K) F (P)) meet (K) W = P meet (K) W$
22	1 11 2 3 4	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P meet (K) W = \underset{˙}{0}$
23	7 9 22	syl2anc	$⊢ ((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 P meet (K) W = \underset{˙}{0}$
24	13 21 23	3eqtrd	$⊢ ((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) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem trl0

Proof