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 ⊢ H = LHyp ⁡ K
ltrnldil.d ⊢ D = LDil ⁡ K ⁡ W
ltrnldil.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnldil ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ 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 ⊢ ≤ K = ≤ 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 ∈ V ∧ W ∈ H → F ∈ T ↔ F ∈ D ∧ ∀ p ∈ Atoms ⁡ K ∀ q ∈ Atoms ⁡ K ¬ p ≤ K W ∧ ¬ q ≤ K W → p join ⁡ K F ⁡ p meet ⁡ K W = q join ⁡ K F ⁡ q meet ⁡ K W
9 8 simprbda ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ D