Theorem ltrnldil

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

	Ref	Expression
Hypotheses	ltrnldil.h	|- H = ( LHyp ` K )
	ltrnldil.d	|- D = ( ( LDil ` K ) ` W )
	ltrnldil.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrnldil	|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. D )

Proof

Step	Hyp	Ref	Expression
1		ltrnldil.h	|- H = ( LHyp ` K )
2		ltrnldil.d	|- D = ( ( LDil ` K ) ` W )
3		ltrnldil.t	|- T = ( ( LTrn ` K ) ` W )
4		eqid	|- ( le ` K ) = ( le ` K )
5		eqid	|- ( join ` K ) = ( join ` K )
6		eqid	|- ( meet ` K ) = ( meet ` K )
7		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
8	4 5 6 7 1 2 3	isltrn	|- ( ( K e. V /\ W e. H ) -> ( F e. T <-> ( F e. D /\ A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) ( ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) -> ( ( p ( join ` K ) ( F ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( F ` q ) ) ( meet ` K ) W ) ) ) ) )
9	8	simprbda	|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. D )