Theorem ltrnlaut

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

	Ref	Expression
Hypotheses	ltrnlaut.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnlaut.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
	ltrnlaut.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnlaut	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in I$$

Proof

Step	Hyp	Ref	Expression
1		ltrnlaut.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		ltrnlaut.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
3		ltrnlaut.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		eqid	$$⊢\mathrm{LDil}\left(K\right)\left(W\right)=\mathrm{LDil}\left(K\right)\left(W\right)$$
5	1 4 3	ltrnldil	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in \mathrm{LDil}\left(K\right)\left(W\right)$$
6	1 2 4	ldillaut	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in \mathrm{LDil}\left(K\right)\left(W\right)\right)\to F\in I$$
7	5 6	syldan	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in I$$