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

Theorem trlnidatb 30974
 Description: A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 30970? Why do both this and ltrnideq 30972 need trlnidat 30970? (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 30970 . . 3
763expia 1155 . 2
8 eqid 2436 . . . . . 6
98, 2, 3lhpexnle 30803 . . . . 5
109adantr 452 . . . 4
111, 8, 2, 3, 4ltrnideq 30972 . . . . . 6
12113expa 1153 . . . . 5
13 simp1l 981 . . . . . . . 8
14 simp2 958 . . . . . . . 8
15 simp1r 982 . . . . . . . 8
16 simp3 959 . . . . . . . 8
17 eqid 2436 . . . . . . . . 9
188, 17, 2, 3, 4, 5trl0 30967 . . . . . . . 8
1913, 14, 15, 16, 18syl112anc 1188 . . . . . . 7
20193expia 1155 . . . . . 6
21 simplll 735 . . . . . . . 8
22 hlatl 30158 . . . . . . . 8
2317, 2atn0 30106 . . . . . . . . 9
2423ex 424 . . . . . . . 8
2521, 22, 243syl 19 . . . . . . 7
2625necon2bd 2653 . . . . . 6
2720, 26syld 42 . . . . 5
2812, 27sylbid 207 . . . 4
2910, 28rexlimddv 2834 . . 3