This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgcpbl

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 efgcpbl ⊢ A ∈ W ∧ B ∈ W ∧ X ∼ ˙ Y → A ++ X ++ B ∼ ˙ A ++ Y ++ B

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 eqid ⊢ i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B = i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B
8 1 2 3 4 5 6 7 efgcpbllemb ⊢ A ∈ W ∧ B ∈ W → ∼ ˙ ⊆ i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B
9 8 ssbrd ⊢ A ∈ W ∧ B ∈ W → X ∼ ˙ Y → X i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B Y
10 9 3impia ⊢ A ∈ W ∧ B ∈ W ∧ X ∼ ˙ Y → X i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B Y
11 1 2 3 4 5 6 7 efgcpbllema ⊢ X i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B Y ↔ X ∈ W ∧ Y ∈ W ∧ A ++ X ++ B ∼ ˙ A ++ Y ++ B
12 11 simp3bi ⊢ X i j | i j ⊆ W ∧ A ++ i ++ B ∼ ˙ A ++ j ++ B Y → A ++ X ++ B ∼ ˙ A ++ Y ++ B
13 10 12 syl ⊢ A ∈ W ∧ B ∈ W ∧ X ∼ ˙ Y → A ++ X ++ B ∼ ˙ A ++ Y ++ B