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 \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	efgcpbl2	$⊢ (A \underset{˙}{\sim} X \land B \underset{˙}{\sim} Y) \to (A ++ B) \underset{˙}{\sim} (X ++ Y)$

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

Metamath Proof Explorer

Theorem efgcpbl2

Proof