Theorem ltrnldil

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

	Ref	Expression
Hypotheses	ltrnldil.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnldil.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
	ltrnldil.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnldil	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in D$$

Proof

Step	Hyp	Ref	Expression
1		ltrnldil.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		ltrnldil.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
3		ltrnldil.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
6		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
7		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
8	4 5 6 7 1 2 3	isltrn	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\wedge \forall p\in \mathrm{Atoms}\left(K\right)\forall q\in \mathrm{Atoms}\left(K\right)\left(\left(\neg p{\le }_{K}W\wedge \neg q{\le }_{K}W\right)\to \left(p\mathrm{join}\left(K\right)F\left(p\right)\right)\mathrm{meet}\left(K\right)W=\left(q\mathrm{join}\left(K\right)F\left(q\right)\right)\mathrm{meet}\left(K\right)W\right)\right)\right)$$
9	8	simprbda	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in D$$