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

Metamath Proof Explorer

Theorem ldillaut

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

Ref Expression
Hypotheses ldillaut.h ⊢ H = LHyp ⁡ K
ldillaut.i ⊢ I = LAut ⁡ K
ldillaut.d ⊢ D = LDil ⁡ K ⁡ W
Assertion ldillaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → F ∈ I

Proof

Step Hyp Ref Expression
1 ldillaut.h ⊢ H = LHyp ⁡ K
2 ldillaut.i ⊢ I = LAut ⁡ K
3 ldillaut.d ⊢ D = LDil ⁡ K ⁡ W
4 eqid ⊢ Base K = Base K
5 eqid ⊢ ≤ K = ≤ K
6 4 5 1 2 3 isldil ⊢ K ∈ V ∧ W ∈ H → F ∈ D ↔ F ∈ I ∧ ∀ x ∈ Base K x ≤ K W → F ⁡ x = x
7 6 simprbda ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → F ∈ I