This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝐷 )