Metamath Proof Explorer

Theorem efgrelexlema

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
efgrelexlem.1 ⊢ L = i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0
Assertion efgrelexlema ⊢ A L 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 efgrelexlem.1 ⊢ L = i j | ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0
8 7 bropaex12 ⊢ A L B → A ∈ V ∧ B ∈ V
9 n0i ⊢ a ∈ S -1 A → ¬ S -1 A = ∅
10 snprc ⊢ ¬ A ∈ V ↔ A = ∅
11 imaeq2 ⊢ A = ∅ → S -1 A = S -1 ∅
12 10 11 sylbi ⊢ ¬ A ∈ V → S -1 A = S -1 ∅
13 ima0 ⊢ S -1 ∅ = ∅
14 12 13 eqtrdi ⊢ ¬ A ∈ V → S -1 A = ∅
15 9 14 nsyl2 ⊢ a ∈ S -1 A → A ∈ V
16 n0i ⊢ b ∈ S -1 B → ¬ S -1 B = ∅
17 snprc ⊢ ¬ B ∈ V ↔ B = ∅
18 imaeq2 ⊢ B = ∅ → S -1 B = S -1 ∅
19 17 18 sylbi ⊢ ¬ B ∈ V → S -1 B = S -1 ∅
20 19 13 eqtrdi ⊢ ¬ B ∈ V → S -1 B = ∅
21 16 20 nsyl2 ⊢ b ∈ S -1 B → B ∈ V
22 15 21 anim12i ⊢ a ∈ S -1 A ∧ b ∈ S -1 B → A ∈ V ∧ B ∈ V
23 22 a1d ⊢ a ∈ S -1 A ∧ b ∈ S -1 B → a ⁡ 0 = b ⁡ 0 → A ∈ V ∧ B ∈ V
24 23 rexlimivv ⊢ ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0 → A ∈ V ∧ B ∈ V
25 fveq1 ⊢ c = a → c ⁡ 0 = a ⁡ 0
26 25 eqeq1d ⊢ c = a → c ⁡ 0 = d ⁡ 0 ↔ a ⁡ 0 = d ⁡ 0
27 fveq1 ⊢ d = b → d ⁡ 0 = b ⁡ 0
28 27 eqeq2d ⊢ d = b → a ⁡ 0 = d ⁡ 0 ↔ a ⁡ 0 = b ⁡ 0
29 26 28 cbvrex2vw ⊢ ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0 ↔ ∃ a ∈ S -1 i ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0
30 sneq ⊢ i = A → i = A
31 30 imaeq2d ⊢ i = A → S -1 i = S -1 A
32 31 rexeqdv ⊢ i = A → ∃ a ∈ S -1 i ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0 ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0
33 29 32 bitrid ⊢ i = A → ∃ c ∈ S -1 i ∃ d ∈ S -1 j c ⁡ 0 = d ⁡ 0 ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0
34 sneq ⊢ j = B → j = B
35 34 imaeq2d ⊢ j = B → S -1 j = S -1 B
36 35 rexeqdv ⊢ j = B → ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0 ↔ ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0
37 36 rexbidv ⊢ j = B → ∃ a ∈ S -1 A ∃ b ∈ S -1 j a ⁡ 0 = b ⁡ 0 ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0
38 33 37 7 brabg ⊢ A ∈ V ∧ B ∈ V → A L B ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0
39 8 24 38 pm5.21nii ⊢ A L B ↔ ∃ a ∈ S -1 A ∃ b ∈ S -1 B a ⁡ 0 = b ⁡ 0