trlatn0

Description: The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trl0a.z	$⊢ \underset{˙}{0} = 0. (K)$
	trl0a.a	$⊢ A = Atoms (K)$
	trl0a.h	$⊢ H = LHyp (K)$
	trl0a.t	$⊢ T = LTrn (K) (W)$
	trl0a.r	$⊢ R = trL (K) (W)$
Assertion	trlatn0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \leftrightarrow R (F) \neq \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		trl0a.z	$⊢ \underset{˙}{0} = 0. (K)$
2		trl0a.a	$⊢ A = Atoms (K)$
3		trl0a.h	$⊢ H = LHyp (K)$
4		trl0a.t	$⊢ T = LTrn (K) (W)$
5		trl0a.r	$⊢ R = trL (K) (W)$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land R (F) \in A) \to K \in AtLat$
8	1 2	atn0	$⊢ (K \in AtLat \land R (F) \in A) \to R (F) \neq \underset{˙}{0}$
9	7 8	sylancom	$⊢ (((K \in HL \land W \in H) \land F \in T) \land R (F) \in A) \to R (F) \neq \underset{˙}{0}$
10	9	ex	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \to R (F) \neq \underset{˙}{0})$
11	1 2 3 4 5	trlator0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \lor R (F) = \underset{˙}{0})$
12	11	ord	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\neg R (F) \in A \to R (F) = \underset{˙}{0})$
13	12	necon1ad	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \neq \underset{˙}{0} \to R (F) \in A)$
14	10 13	impbid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \leftrightarrow R (F) \neq \underset{˙}{0})$

Metamath Proof Explorer