Description: Define set of all lattice translations. Similar to definition of translation in Crawley p. 111. (Contributed by NM, 11-May-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ltrn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cltrn | |
|
1 | vk | |
|
2 | cvv | |
|
3 | vw | |
|
4 | clh | |
|
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | vf | |
|
8 | cldil | |
|
9 | 5 8 | cfv | |
10 | 3 | cv | |
11 | 10 9 | cfv | |
12 | vp | |
|
13 | catm | |
|
14 | 5 13 | cfv | |
15 | vq | |
|
16 | 12 | cv | |
17 | cple | |
|
18 | 5 17 | cfv | |
19 | 16 10 18 | wbr | |
20 | 19 | wn | |
21 | 15 | cv | |
22 | 21 10 18 | wbr | |
23 | 22 | wn | |
24 | 20 23 | wa | |
25 | cjn | |
|
26 | 5 25 | cfv | |
27 | 7 | cv | |
28 | 16 27 | cfv | |
29 | 16 28 26 | co | |
30 | cmee | |
|
31 | 5 30 | cfv | |
32 | 29 10 31 | co | |
33 | 21 27 | cfv | |
34 | 21 33 26 | co | |
35 | 34 10 31 | co | |
36 | 32 35 | wceq | |
37 | 24 36 | wi | |
38 | 37 15 14 | wral | |
39 | 38 12 14 | wral | |
40 | 39 7 11 | crab | |
41 | 3 6 40 | cmpt | |
42 | 1 2 41 | cmpt | |
43 | 0 42 | wceq | |