Metamath Proof Explorer


Theorem ldillaut

Description: A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ldillaut.h H = LHyp K
ldillaut.i I = LAut K
ldillaut.d D = LDil K W
Assertion ldillaut K V W H F D F I

Proof

Step Hyp Ref Expression
1 ldillaut.h H = LHyp K
2 ldillaut.i I = LAut K
3 ldillaut.d D = LDil K W
4 eqid Base K = Base K
5 eqid K = K
6 4 5 1 2 3 isldil K V W H F D F I x Base K x K W F x = x
7 6 simprbda K V W H F D F I