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 | ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝐼 ) |
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 | ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝐼 ) |