Metamath Proof Explorer

Theorem ltrn11

Description: One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrn1o.b ⊢ B = Base K
ltrn1o.h ⊢ H = LHyp ⁡ K
ltrn1o.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrn11 ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ⁡ X = F ⁡ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 ltrn1o.b ⊢ B = Base K
2 ltrn1o.h ⊢ H = LHyp ⁡ K
3 ltrn1o.t ⊢ T = LTrn ⁡ K ⁡ W
4 simp1l ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → K ∈ V
5 eqid ⊢ LAut ⁡ K = LAut ⁡ K
6 2 5 3 ltrnlaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ LAut ⁡ K
7 6 3adant3 ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ∈ LAut ⁡ K
8 simp3l ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ∈ B
9 simp3r ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
10 1 5 laut11 ⊢ K ∈ V ∧ F ∈ LAut ⁡ K ∧ X ∈ B ∧ Y ∈ B → F ⁡ X = F ⁡ Y ↔ X = Y
11 4 7 8 9 10 syl22anc ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ⁡ X = F ⁡ Y ↔ X = Y