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 \times 2_{𝑜}))$
		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
	Assertion	efgcpbl	$⊢ (A \in W \land B \in W \land X \underset{˙}{\sim} Y) \to ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B)$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7		eqid	$⊢ \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} = \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
8	1 2 3 4 5 6 7	efgcpbllemb	$⊢ (A \in W \land B \in W) \to \underset{˙}{\sim} \subseteq \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
9	8	ssbrd	$⊢ (A \in W \land B \in W) \to (X \underset{˙}{\sim} Y \to X \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} Y)$
10	9	3impia	$⊢ (A \in W \land B \in W \land X \underset{˙}{\sim} Y) \to X \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} Y$
11	1 2 3 4 5 6 7	efgcpbllema	$⊢ X \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} Y \leftrightarrow (X \in W \land Y \in W \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$
12	11	simp3bi	$⊢ X \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} Y \to ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B)$
13	10 12	syl	$⊢ (A \in W \land B \in W \land X \underset{˙}{\sim} Y) \to ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B)$