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⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
efgrelexlem.1 ⊢L=ij|∃c∈S-1i∃d∈S-1jc⁡0=d⁡0
Assertion efgrelexlema ⊢ALB↔∃a∈S-1A∃b∈S-1Ba⁡0=b⁡0

Proof

Step Hyp Ref Expression
1 efgval.w ⊢W=I⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
7 efgrelexlem.1 ⊢L=ij|∃c∈S-1i∃d∈S-1jc⁡0=d⁡0
8 7 bropaex12 ⊢ALB→A∈V∧B∈V
9 n0i ⊢a∈S-1A→¬S-1A=∅
10 snprc ⊢¬A∈V↔A=∅
11 imaeq2 ⊢A=∅→S-1A=S-1∅
12 10 11 sylbi ⊢¬A∈V→S-1A=S-1∅
13 ima0 ⊢S-1∅=∅
14 12 13 eqtrdi ⊢¬A∈V→S-1A=∅
15 9 14 nsyl2 ⊢a∈S-1A→A∈V
16 n0i ⊢b∈S-1B→¬S-1B=∅
17 snprc ⊢¬B∈V↔B=∅
18 imaeq2 ⊢B=∅→S-1B=S-1∅
19 17 18 sylbi ⊢¬B∈V→S-1B=S-1∅
20 19 13 eqtrdi ⊢¬B∈V→S-1B=∅
21 16 20 nsyl2 ⊢b∈S-1B→B∈V
22 15 21 anim12i ⊢a∈S-1A∧b∈S-1B→A∈V∧B∈V
23 22 a1d ⊢a∈S-1A∧b∈S-1B→a⁡0=b⁡0→A∈V∧B∈V
24 23 rexlimivv ⊢∃a∈S-1A∃b∈S-1Ba⁡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-1i∃d∈S-1jc⁡0=d⁡0↔∃a∈S-1i∃b∈S-1ja⁡0=b⁡0
30 sneq ⊢i=A→i=A
31 30 imaeq2d ⊢i=A→S-1i=S-1A
32 31 rexeqdv ⊢i=A→∃a∈S-1i∃b∈S-1ja⁡0=b⁡0↔∃a∈S-1A∃b∈S-1ja⁡0=b⁡0
33 29 32 bitrid ⊢i=A→∃c∈S-1i∃d∈S-1jc⁡0=d⁡0↔∃a∈S-1A∃b∈S-1ja⁡0=b⁡0
34 sneq ⊢j=B→j=B
35 34 imaeq2d ⊢j=B→S-1j=S-1B
36 35 rexeqdv ⊢j=B→∃b∈S-1ja⁡0=b⁡0↔∃b∈S-1Ba⁡0=b⁡0
37 36 rexbidv ⊢j=B→∃a∈S-1A∃b∈S-1ja⁡0=b⁡0↔∃a∈S-1A∃b∈S-1Ba⁡0=b⁡0
38 33 37 7 brabg ⊢A∈V∧B∈V→ALB↔∃a∈S-1A∃b∈S-1Ba⁡0=b⁡0
39 8 24 38 pm5.21nii ⊢ALB↔∃a∈S-1A∃b∈S-1Ba⁡0=b⁡0