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 e. V /\ W e. H ) /\ F e. T ) -> F e. 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 e. V /\ W e. H ) /\ F e. T ) -> F e. ( ( LDil ` K ) ` W ) )
6 1 2 4 ldillaut
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. ( ( LDil ` K ) ` W ) ) -> F e. I )
7 5 6 syldan
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. I )