# 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}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
Assertion efgrelex

### Proof

Step Hyp Ref Expression
1 efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 efgval.r
3 efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
4 efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
5 efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
6 efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
7 eqid ${⊢}\left\{⟨{i},{j}⟩|\exists {c}\in {{S}}^{-1}\left[\left\{{i}\right\}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {{S}}^{-1}\left[\left\{{j}\right\}\right]\phantom{\rule{.4em}{0ex}}{c}\left(0\right)={d}\left(0\right)\right\}=\left\{⟨{i},{j}⟩|\exists {c}\in {{S}}^{-1}\left[\left\{{i}\right\}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {{S}}^{-1}\left[\left\{{j}\right\}\right]\phantom{\rule{.4em}{0ex}}{c}\left(0\right)={d}\left(0\right)\right\}$
8 1 2 3 4 5 6 7 efgrelexlemb
9 8 ssbri
10 1 2 3 4 5 6 7 efgrelexlema ${⊢}{A}\left\{⟨{i},{j}⟩|\exists {c}\in {{S}}^{-1}\left[\left\{{i}\right\}\right]\phantom{\rule{.4em}{0ex}}\exists {d}\in {{S}}^{-1}\left[\left\{{j}\right\}\right]\phantom{\rule{.4em}{0ex}}{c}\left(0\right)={d}\left(0\right)\right\}{B}↔\exists {a}\in {{S}}^{-1}\left[\left\{{A}\right\}\right]\phantom{\rule{.4em}{0ex}}\exists {b}\in {{S}}^{-1}\left[\left\{{B}\right\}\right]\phantom{\rule{.4em}{0ex}}{a}\left(0\right)={b}\left(0\right)$
11 9 10 sylib