Metamath Proof Explorer

Theorem efgrelex

Description: If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A , b ends at B , and a and B have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
Assertion efgrelex ⊢ A ∼ ˙ B → ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
6 efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
7 eqid ⊢ i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0 = i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0
8 1 2 3 4 5 6 7 efgrelexlemb ⊢ ∼ ˙ ⊆ i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0
9 8 ssbri ⊢ A ∼ ˙ B → A i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0 B
10 1 2 3 4 5 6 7 efgrelexlema ⊢ A i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0 B ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0
11 9 10 sylib ⊢ A ∼ ˙ B → ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0