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

Theorem trlnidatb 33814
 Description: A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 33810? Why do both this and ltrnideq 33812 need trlnidat 33810? (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 33810 . . 3
763expia 1233 . 2
8 eqid 2471 . . . . . 6
98, 2, 3lhpexnle 33642 . . . . 5
109adantr 472 . . . 4
111, 8, 2, 3, 4ltrnideq 33812 . . . . . 6
12113expa 1231 . . . . 5
13 simp1l 1054 . . . . . . . 8
14 simp2 1031 . . . . . . . 8
15 simp1r 1055 . . . . . . . 8
16 simp3 1032 . . . . . . . 8
17 eqid 2471 . . . . . . . . 9
188, 17, 2, 3, 4, 5trl0 33807 . . . . . . . 8
1913, 14, 15, 16, 18syl112anc 1296 . . . . . . 7
20193expia 1233 . . . . . 6
21 simplll 776 . . . . . . . 8
22 hlatl 32997 . . . . . . . 8
2317, 2atn0 32945 . . . . . . . . 9
2423ex 441 . . . . . . . 8
2521, 22, 243syl 18 . . . . . . 7
2625necon2bd 2659 . . . . . 6
2720, 26syld 44 . . . . 5
2812, 27sylbid 223 . . . 4
2910, 28rexlimddv 2875 . . 3