English
A refinement of the normal-word existence statement specialized to a parameterized φ and transversal d, ensuring the same φ-image and a structural match for the first-coordinate list, with heads satisfying subgroup inclusion for all first entries.
Русский
Уточнение существования нормального слова, специфичное для параметризации φ и трансверсала d, сохраняющее образ φ и соответствующую структуру списка первых координат, с головой, удовлетворяющей включению в подгруппу для всех первых элементов.
LaTeX
$$$\\exists w' : NormalWord(d), \n w'.prod φ = w.prod φ ∧\n w'.toList.map Prod.fst = w.toList.map Prod.fst ∧\n \\forall u ∈ w.toList.head?.map Prod.fst,\\, w'.head ∈ toSubgroup A B (-u).$$$
Lean4
/-- **Britton's Lemma**. Any reduced word whose product is an element of `G`, has no
occurrences of `t`. -/
theorem toList_eq_nil_of_mem_of_range (w : ReducedWord G A B)
(hw : w.prod φ ∈ (of.range : Subgroup (HNNExtension G A B φ))) : w.toList = [] :=
by
rcases hw with ⟨g, hg⟩
let w' : ReducedWord G A B := { ReducedWord.empty G A B with head := g }
have : w.prod φ = w'.prod φ := by simp [w', ReducedWord.prod, hg]
simpa [w'] using (map_fst_eq_and_of_prod_eq φ this).1
