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 ) |
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 ) |