Metamath Proof Explorer


Theorem 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 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 HL W H F T R F A R F 0 ˙

Proof

Step Hyp Ref Expression
1 trl0a.z 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 HL K AtLat
7 6 ad3antrrr K HL W H F T R F A K AtLat
8 1 2 atn0 K AtLat R F A R F 0 ˙
9 7 8 sylancom K HL W H F T R F A R F 0 ˙
10 9 ex K HL W H F T R F A R F 0 ˙
11 1 2 3 4 5 trlator0 K HL W H F T R F A R F = 0 ˙
12 11 ord K HL W H F T ¬ R F A R F = 0 ˙
13 12 necon1ad K HL W H F T R F 0 ˙ R F A
14 10 13 impbid K HL W H F T R F A R F 0 ˙