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 e. V /\ W e. H ) /\ F e. D ) -> F e. 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	|- ( le ` K ) = ( le ` K )
6	4 5 1 2 3	isldil	|- ( ( K e. V /\ W e. H ) -> ( F e. D <-> ( F e. I /\ A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( F ` x ) = x ) ) ) )
7	6	simprbda	|- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F e. I )