Theorem ldillaut

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

	Ref	Expression
Hypotheses	ldillaut.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ldillaut.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
	ldillaut.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
Assertion	ldillaut	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in D\right)\to F\in I$$

Proof

Step	Hyp	Ref	Expression
1		ldillaut.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		ldillaut.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
3		ldillaut.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6	4 5 1 2 3	isldil	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in D\leftrightarrow \left(F\in I\wedge \forall x\in {\mathrm{Base}}_K\left(x{\le }_{K}W\to F\left(x\right)=x\right)\right)\right)$$
7	6	simprbda	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in D\right)\to F\in I$$