Description: The identity function is a lattice dilation. (Contributed by NM, 18-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | idldil.b | |
|
idldil.h | |
||
idldil.d | |
||
Assertion | idldil | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idldil.b | |
|
2 | idldil.h | |
|
3 | idldil.d | |
|
4 | eqid | |
|
5 | 1 4 | idlaut | |
6 | 5 | adantr | |
7 | fvresi | |
|
8 | 7 | a1d | |
9 | 8 | rgen | |
10 | 9 | a1i | |
11 | eqid | |
|
12 | 1 11 2 4 3 | isldil | |
13 | 6 10 12 | mpbir2and | |