Metamath Proof Explorer


Theorem ltrnlaut

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

Ref Expression
Hypotheses ltrnlaut.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnlaut.i 𝐼 = ( LAut ‘ 𝐾 )
ltrnlaut.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnlaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹𝐼 )

Proof

Step Hyp Ref Expression
1 ltrnlaut.h 𝐻 = ( LHyp ‘ 𝐾 )
2 ltrnlaut.i 𝐼 = ( LAut ‘ 𝐾 )
3 ltrnlaut.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
5 1 4 3 ltrnldil ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) )
6 1 2 4 ldillaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐹𝐼 )
7 5 6 syldan ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹𝐼 )