Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trlnidatb Unicode version

Theorem trlnidatb 30366
 Description: A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 30362? Why do both this and ltrnideq 30364 need trlnidat 30362? (Contributed by NM, 4-Jun-2013.)
Hypotheses
Ref Expression
trlnidatb.b
trlnidatb.a
trlnidatb.h
trlnidatb.t
trlnidatb.r
Assertion
Ref Expression
trlnidatb

Proof of Theorem trlnidatb
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 trlnidatb.b . . . 4
2 trlnidatb.a . . . 4
3 trlnidatb.h . . . 4
4 trlnidatb.t . . . 4
5 trlnidatb.r . . . 4
61, 2, 3, 4, 5trlnidat 30362 . . 3
763expia 1153 . 2
8 eqid 2283 . . . . . 6
98, 2, 3lhpexnle 30195 . . . . 5
109adantr 451 . . . 4
111, 8, 2, 3, 4ltrnideq 30364 . . . . . . . 8
12113expa 1151 . . . . . . 7
13 simp1l 979 . . . . . . . . . 10
14 simp2 956 . . . . . . . . . 10
15 simp1r 980 . . . . . . . . . 10
16 simp3 957 . . . . . . . . . 10
17 eqid 2283 . . . . . . . . . . 11
188, 17, 2, 3, 4, 5trl0 30359 . . . . . . . . . 10
1913, 14, 15, 16, 18syl112anc 1186 . . . . . . . . 9
20193expia 1153 . . . . . . . 8
21 simplll 734 . . . . . . . . . 10
22 hlatl 29550 . . . . . . . . . 10
2317, 2atn0 29498 . . . . . . . . . . 11
2423ex 423 . . . . . . . . . 10
2521, 22, 243syl 18 . . . . . . . . 9
2625necon2bd 2495 . . . . . . . 8
2720, 26syld 40 . . . . . . 7
2812, 27sylbid 206 . . . . . 6
2928exp32 588 . . . . 5
3029rexlimdv 2666 . . . 4
3110, 30mpd 14 . . 3