Theorem ltrnldil

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

	Ref	Expression
Hypotheses	ltrnldil.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	ltrnldil.d	⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
	ltrnldil.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion	ltrnldil	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		ltrnldil.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		ltrnldil.d	⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
3		ltrnldil.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
7		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8	4 5 6 7 1 2 3	isltrn	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑝 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑞 ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
9	8	simprbda	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝐷 )