Description: A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ldillaut.h | ||
ldillaut.i | |||
ldillaut.d | |||
Assertion | ldillaut |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ldillaut.h | ||
2 | ldillaut.i | ||
3 | ldillaut.d | ||
4 | eqid | ||
5 | eqid | ||
6 | 4 5 1 2 3 | isldil | |
7 | 6 | simprbda |