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

Metamath Proof Explorer

Theorem ltrnlaut

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

Ref Expression
Hypotheses ltrnlaut.h ⊢ H = LHyp ⁡ K
ltrnlaut.i ⊢ I = LAut ⁡ K
ltrnlaut.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnlaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ I

Proof

Step Hyp Ref Expression
1 ltrnlaut.h ⊢ H = LHyp ⁡ K
2 ltrnlaut.i ⊢ I = LAut ⁡ K
3 ltrnlaut.t ⊢ T = LTrn ⁡ K ⁡ W
4 eqid ⊢ LDil ⁡ K ⁡ W = LDil ⁡ K ⁡ W
5 1 4 3 ltrnldil ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ LDil ⁡ K ⁡ W
6 1 2 4 ldillaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ LDil ⁡ K ⁡ W → F ∈ I
7 5 6 syldan ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ I