Description: The identity function is a lattice translation. Remark below Lemma B in Crawley p. 112. (Contributed by NM, 18-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | idltrn.b | |
|
idltrn.h | |
||
idltrn.t | |
||
Assertion | idltrn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idltrn.b | |
|
2 | idltrn.h | |
|
3 | idltrn.t | |
|
4 | eqid | |
|
5 | 1 2 4 | idldil | |
6 | simpll | |
|
7 | simplrr | |
|
8 | simprr | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 9 10 11 12 2 | lhpmat | |
14 | 6 7 8 13 | syl12anc | |
15 | 1 12 | atbase | |
16 | fvresi | |
|
17 | 7 15 16 | 3syl | |
18 | 17 | oveq2d | |
19 | simplll | |
|
20 | eqid | |
|
21 | 20 12 | hlatjidm | |
22 | 19 7 21 | syl2anc | |
23 | 18 22 | eqtrd | |
24 | 23 | oveq1d | |
25 | simplrl | |
|
26 | 1 12 | atbase | |
27 | fvresi | |
|
28 | 25 26 27 | 3syl | |
29 | 28 | oveq2d | |
30 | 20 12 | hlatjidm | |
31 | 19 25 30 | syl2anc | |
32 | 29 31 | eqtrd | |
33 | 32 | oveq1d | |
34 | simprl | |
|
35 | 9 10 11 12 2 | lhpmat | |
36 | 6 25 34 35 | syl12anc | |
37 | 33 36 | eqtrd | |
38 | 14 24 37 | 3eqtr4rd | |
39 | 38 | ex | |
40 | 39 | ralrimivva | |
41 | 9 20 10 12 2 4 3 | isltrn | |
42 | 5 40 41 | mpbir2and | |