efgred2

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	efgred2	$⊢ (A \in dom S \land B \in dom S) \to (S (A) \underset{˙}{\sim} S (B) \leftrightarrow A (0) = B (0))$

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 3 4 5 6	efgsfo	$⊢ S : dom S \underset{onto}{⟶} W$
8		fof	$⊢ S : dom S \underset{onto}{⟶} W \to S : dom S ⟶ W$
9	7 8	ax-mp	$⊢ S : dom S ⟶ W$
10	9	ffvelcdmi	$⊢ B \in dom S \to S (B) \in W$
11	10	ad2antlr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to S (B) \in W$
12	1 2 3 4 5 6	efgredeu	$⊢ S (B) \in W \to \exists! d \in D d \underset{˙}{\sim} S (B)$
13		reurmo	$⊢ \exists! d \in D d \underset{˙}{\sim} S (B) \to \exists^{*} d \in D d \underset{˙}{\sim} S (B)$
14	11 12 13	3syl	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to \exists^{*} d \in D d \underset{˙}{\sim} S (B)$
15	1 2 3 4 5 6	efgsdm	$⊢ A \in dom S \leftrightarrow (A \in (Word W ∖ \{\emptyset\}) \land A (0) \in D \land \forall i \in (1 ..^\|A\|) A (i) \in ran T (A (i - 1)))$
16	15	simp2bi	$⊢ A \in dom S \to A (0) \in D$
17	16	ad2antrr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to A (0) \in D$
18	1 2	efger	$⊢ \underset{˙}{\sim} Er W$
19	18	a1i	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to \underset{˙}{\sim} Er W$
20	1 2 3 4 5 6	efgsrel	$⊢ A \in dom S \to A (0) \underset{˙}{\sim} S (A)$
21	20	ad2antrr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to A (0) \underset{˙}{\sim} S (A)$
22		simpr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to S (A) \underset{˙}{\sim} S (B)$
23	19 21 22	ertrd	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to A (0) \underset{˙}{\sim} S (B)$
24	1 2 3 4 5 6	efgsdm	$⊢ B \in dom S \leftrightarrow (B \in (Word W ∖ \{\emptyset\}) \land B (0) \in D \land \forall i \in (1 ..^\|B\|) B (i) \in ran T (B (i - 1)))$
25	24	simp2bi	$⊢ B \in dom S \to B (0) \in D$
26	25	ad2antlr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to B (0) \in D$
27	1 2 3 4 5 6	efgsrel	$⊢ B \in dom S \to B (0) \underset{˙}{\sim} S (B)$
28	27	ad2antlr	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to B (0) \underset{˙}{\sim} S (B)$
29		breq1	$⊢ d = A (0) \to (d \underset{˙}{\sim} S (B) \leftrightarrow A (0) \underset{˙}{\sim} S (B))$
30		breq1	$⊢ d = B (0) \to (d \underset{˙}{\sim} S (B) \leftrightarrow B (0) \underset{˙}{\sim} S (B))$
31	29 30	rmoi	$⊢ (\exists^{*} d \in D d \underset{˙}{\sim} S (B) \land (A (0) \in D \land A (0) \underset{˙}{\sim} S (B)) \land (B (0) \in D \land B (0) \underset{˙}{\sim} S (B))) \to A (0) = B (0)$
32	14 17 23 26 28 31	syl122anc	$⊢ ((A \in dom S \land B \in dom S) \land S (A) \underset{˙}{\sim} S (B)) \to A (0) = B (0)$
33	18	a1i	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to \underset{˙}{\sim} Er W$
34	20	ad2antrr	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to A (0) \underset{˙}{\sim} S (A)$
35		simpr	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to A (0) = B (0)$
36	27	ad2antlr	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to B (0) \underset{˙}{\sim} S (B)$
37	35 36	eqbrtrd	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to A (0) \underset{˙}{\sim} S (B)$
38	33 34 37	ertr3d	$⊢ ((A \in dom S \land B \in dom S) \land A (0) = B (0)) \to S (A) \underset{˙}{\sim} S (B)$
39	32 38	impbida	$⊢ (A \in dom S \land B \in dom S) \to (S (A) \underset{˙}{\sim} S (B) \leftrightarrow A (0) = B (0))$

Metamath Proof Explorer

Theorem efgred2

Proof