# Metamath Proof Explorer

## Theorem efgcpbl2

Description: Two extension sequences have related endpoints iff they have the same base. (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 efgcpbl2

### 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 1 2 efger
8 7 a1i
9 simpl
10 8 9 ercl
11 wrd0 ${⊢}\varnothing \in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
12 1 efgrcl ${⊢}{A}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
13 10 12 syl
14 13 simprd
15 11 14 eleqtrrid
16 simpr
17 1 2 3 4 5 6 efgcpbl
18 10 15 16 17 syl3anc
19 10 14 eleqtrd
20 8 16 ercl
21 20 14 eleqtrd
22 ccatcl ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
23 19 21 22 syl2anc
24 ccatrid ${⊢}{A}\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left({A}\mathrm{++}{B}\right)\mathrm{++}\varnothing ={A}\mathrm{++}{B}$
25 23 24 syl
26 8 16 ercl2
27 26 14 eleqtrd
28 ccatcl ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {Y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {A}\mathrm{++}{Y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
29 19 27 28 syl2anc
30 ccatrid ${⊢}{A}\mathrm{++}{Y}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left({A}\mathrm{++}{Y}\right)\mathrm{++}\varnothing ={A}\mathrm{++}{Y}$
31 29 30 syl
32 18 25 31 3brtr3d
33 1 2 3 4 5 6 efgcpbl
34 15 26 9 33 syl3anc
35 ccatlid ${⊢}{A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \varnothing \mathrm{++}{A}={A}$
36 19 35 syl
37 36 oveq1d
38 8 9 ercl2
39 38 14 eleqtrd
40 ccatlid ${⊢}{X}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \varnothing \mathrm{++}{X}={X}$
41 39 40 syl
42 41 oveq1d
43 34 37 42 3brtr3d
44 8 32 43 ertrd