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 = 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 efgcpbl2 ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ∼ ˙ X ++ Y

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 1 2 efger ⊢ ∼ ˙ Er W
8 7 a1i ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∼ ˙ Er W
9 simpl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ∼ ˙ X
10 8 9 ercl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ∈ W
11 wrd0 ⊢ ∅ ∈ Word I × 2 𝑜
12 1 efgrcl ⊢ A ∈ W → I ∈ V ∧ W = Word I × 2 𝑜
13 10 12 syl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → I ∈ V ∧ W = Word I × 2 𝑜
14 13 simprd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → W = Word I × 2 𝑜
15 11 14 eleqtrrid ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ∈ W
16 simpr ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → B ∼ ˙ Y
17 1 2 3 4 5 6 efgcpbl ⊢ A ∈ W ∧ ∅ ∈ W ∧ B ∼ ˙ Y → A ++ B ++ ∅ ∼ ˙ A ++ Y ++ ∅
18 10 15 16 17 syl3anc ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ++ ∅ ∼ ˙ A ++ Y ++ ∅
19 10 14 eleqtrd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ∈ Word I × 2 𝑜
20 8 16 ercl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → B ∈ W
21 20 14 eleqtrd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → B ∈ Word I × 2 𝑜
22 ccatcl ⊢ A ∈ Word I × 2 𝑜 ∧ B ∈ Word I × 2 𝑜 → A ++ B ∈ Word I × 2 𝑜
23 19 21 22 syl2anc ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ∈ Word I × 2 𝑜
24 ccatrid ⊢ A ++ B ∈ Word I × 2 𝑜 → A ++ B ++ ∅ = A ++ B
25 23 24 syl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ++ ∅ = A ++ B
26 8 16 ercl2 ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → Y ∈ W
27 26 14 eleqtrd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → Y ∈ Word I × 2 𝑜
28 ccatcl ⊢ A ∈ Word I × 2 𝑜 ∧ Y ∈ Word I × 2 𝑜 → A ++ Y ∈ Word I × 2 𝑜
29 19 27 28 syl2anc ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ Y ∈ Word I × 2 𝑜
30 ccatrid ⊢ A ++ Y ∈ Word I × 2 𝑜 → A ++ Y ++ ∅ = A ++ Y
31 29 30 syl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ Y ++ ∅ = A ++ Y
32 18 25 31 3brtr3d ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ∼ ˙ A ++ Y
33 1 2 3 4 5 6 efgcpbl ⊢ ∅ ∈ W ∧ Y ∈ W ∧ A ∼ ˙ X → ∅ ++ A ++ Y ∼ ˙ ∅ ++ X ++ Y
34 15 26 9 33 syl3anc ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ++ A ++ Y ∼ ˙ ∅ ++ X ++ Y
35 ccatlid ⊢ A ∈ Word I × 2 𝑜 → ∅ ++ A = A
36 19 35 syl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ++ A = A
37 36 oveq1d ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ++ A ++ Y = A ++ Y
38 8 9 ercl2 ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → X ∈ W
39 38 14 eleqtrd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → X ∈ Word I × 2 𝑜
40 ccatlid ⊢ X ∈ Word I × 2 𝑜 → ∅ ++ X = X
41 39 40 syl ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ++ X = X
42 41 oveq1d ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → ∅ ++ X ++ Y = X ++ Y
43 34 37 42 3brtr3d ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ Y ∼ ˙ X ++ Y
44 8 32 43 ertrd ⊢ A ∼ ˙ X ∧ B ∼ ˙ Y → A ++ B ∼ ˙ X ++ Y