efgsrel

Description: The start and end of any extension sequence are related (i.e. evaluate to the same element of the quotient group to be created). (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	efgsrel	$⊢ F \in dom S \to F (0) \underset{˙}{\sim} S (F)$

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	efgsdm	$⊢ F \in dom S \leftrightarrow (F \in (Word W ∖ \{\emptyset\}) \land F (0) \in D \land \forall a \in (1 ..^\|F\|) F (a) \in ran T (F (a - 1)))$
8	7	simp1bi	$⊢ F \in dom S \to F \in (Word W ∖ \{\emptyset\})$
9		eldifsn	$⊢ F \in (Word W ∖ \{\emptyset\}) \leftrightarrow (F \in Word W \land F \neq \emptyset)$
10		lennncl	$⊢ (F \in Word W \land F \neq \emptyset) \to \|F\| \in ℕ$
11	9 10	sylbi	$⊢ F \in (Word W ∖ \{\emptyset\}) \to \|F\| \in ℕ$
12		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
13	8 11 12	3syl	$⊢ F \in dom S \to \|F\| - 1 \in (0 ..^\|F\|)$
14		nnm1nn0	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in ℕ_{0}$
15	8 11 14	3syl	$⊢ F \in dom S \to \|F\| - 1 \in ℕ_{0}$
16		eleq1	$⊢ a = 0 \to (a \in (0 ..^\|F\|) \leftrightarrow 0 \in (0 ..^\|F\|))$
17		fveq2	$⊢ a = 0 \to F (a) = F (0)$
18	17	breq2d	$⊢ a = 0 \to (F (0) \underset{˙}{\sim} F (a) \leftrightarrow F (0) \underset{˙}{\sim} F (0))$
19	16 18	imbi12d	$⊢ a = 0 \to ((a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a)) \leftrightarrow (0 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (0)))$
20	19	imbi2d	$⊢ a = 0 \to ((F \in dom S \to (a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a))) \leftrightarrow (F \in dom S \to (0 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (0))))$
21		eleq1	$⊢ a = i \to (a \in (0 ..^\|F\|) \leftrightarrow i \in (0 ..^\|F\|))$
22		fveq2	$⊢ a = i \to F (a) = F (i)$
23	22	breq2d	$⊢ a = i \to (F (0) \underset{˙}{\sim} F (a) \leftrightarrow F (0) \underset{˙}{\sim} F (i))$
24	21 23	imbi12d	$⊢ a = i \to ((a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a)) \leftrightarrow (i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)))$
25	24	imbi2d	$⊢ a = i \to ((F \in dom S \to (a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a))) \leftrightarrow (F \in dom S \to (i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i))))$
26		eleq1	$⊢ a = i + 1 \to (a \in (0 ..^\|F\|) \leftrightarrow i + 1 \in (0 ..^\|F\|))$
27		fveq2	$⊢ a = i + 1 \to F (a) = F (i + 1)$
28	27	breq2d	$⊢ a = i + 1 \to (F (0) \underset{˙}{\sim} F (a) \leftrightarrow F (0) \underset{˙}{\sim} F (i + 1))$
29	26 28	imbi12d	$⊢ a = i + 1 \to ((a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a)) \leftrightarrow (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1)))$
30	29	imbi2d	$⊢ a = i + 1 \to ((F \in dom S \to (a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a))) \leftrightarrow (F \in dom S \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1))))$
31		eleq1	$⊢ a = \|F\| - 1 \to (a \in (0 ..^\|F\|) \leftrightarrow \|F\| - 1 \in (0 ..^\|F\|))$
32		fveq2	$⊢ a = \|F\| - 1 \to F (a) = F (\|F\| - 1)$
33	32	breq2d	$⊢ a = \|F\| - 1 \to (F (0) \underset{˙}{\sim} F (a) \leftrightarrow F (0) \underset{˙}{\sim} F (\|F\| - 1))$
34	31 33	imbi12d	$⊢ a = \|F\| - 1 \to ((a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a)) \leftrightarrow (\|F\| - 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (\|F\| - 1)))$
35	34	imbi2d	$⊢ a = \|F\| - 1 \to ((F \in dom S \to (a \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (a))) \leftrightarrow (F \in dom S \to (\|F\| - 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (\|F\| - 1))))$
36	1 2	efger	$⊢ \underset{˙}{\sim} Er W$
37	36	a1i	$⊢ (F \in dom S \land 0 \in (0 ..^\|F\|)) \to \underset{˙}{\sim} Er W$
38		eldifi	$⊢ F \in (Word W ∖ \{\emptyset\}) \to F \in Word W$
39		wrdf	$⊢ F \in Word W \to F : (0 ..^\|F\|) ⟶ W$
40	8 38 39	3syl	$⊢ F \in dom S \to F : (0 ..^\|F\|) ⟶ W$
41	40	ffvelcdmda	$⊢ (F \in dom S \land 0 \in (0 ..^\|F\|)) \to F (0) \in W$
42	37 41	erref	$⊢ (F \in dom S \land 0 \in (0 ..^\|F\|)) \to F (0) \underset{˙}{\sim} F (0)$
43	42	ex	$⊢ F \in dom S \to (0 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (0))$
44		elnn0uz	$⊢ i \in ℕ_{0} \leftrightarrow i \in ℤ_{\geq 0}$
45		peano2fzor	$⊢ (i \in ℤ_{\geq 0} \land i + 1 \in (0 ..^\|F\|)) \to i \in (0 ..^\|F\|)$
46	44 45	sylanb	$⊢ (i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i \in (0 ..^\|F\|)$
47	46	3adant1	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i \in (0 ..^\|F\|)$
48	47	3expia	$⊢ (F \in dom S \land i \in ℕ_{0}) \to (i + 1 \in (0 ..^\|F\|) \to i \in (0 ..^\|F\|))$
49	48	imim1d	$⊢ (F \in dom S \land i \in ℕ_{0}) \to ((i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)) \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)))$
50	40	3ad2ant1	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F : (0 ..^\|F\|) ⟶ W$
51	50 47	ffvelcdmd	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F (i) \in W$
52		fvoveq1	$⊢ a = i + 1 \to F (a - 1) = F (i + 1 - 1)$
53	52	fveq2d	$⊢ a = i + 1 \to T (F (a - 1)) = T (F (i + 1 - 1))$
54	53	rneqd	$⊢ a = i + 1 \to ran T (F (a - 1)) = ran T (F (i + 1 - 1))$
55	27 54	eleq12d	$⊢ a = i + 1 \to (F (a) \in ran T (F (a - 1)) \leftrightarrow F (i + 1) \in ran T (F (i + 1 - 1)))$
56	7	simp3bi	$⊢ F \in dom S \to \forall a \in (1 ..^\|F\|) F (a) \in ran T (F (a - 1))$
57	56	3ad2ant1	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to \forall a \in (1 ..^\|F\|) F (a) \in ran T (F (a - 1))$
58		nn0p1nn	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ$
59	58	3ad2ant2	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i + 1 \in ℕ$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61	59 60	eleqtrdi	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i + 1 \in ℤ_{\geq 1}$
62		elfzolt2b	$⊢ i + 1 \in (0 ..^\|F\|) \to i + 1 \in (i + 1 ..^\|F\|)$
63	62	3ad2ant3	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i + 1 \in (i + 1 ..^\|F\|)$
64		elfzo3	$⊢ i + 1 \in (1 ..^\|F\|) \leftrightarrow (i + 1 \in ℤ_{\geq 1} \land i + 1 \in (i + 1 ..^\|F\|))$
65	61 63 64	sylanbrc	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i + 1 \in (1 ..^\|F\|)$
66	55 57 65	rspcdva	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F (i + 1) \in ran T (F (i + 1 - 1))$
67		nn0cn	$⊢ i \in ℕ_{0} \to i \in ℂ$
68	67	3ad2ant2	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i \in ℂ$
69		ax-1cn	$⊢ 1 \in ℂ$
70		pncan	$⊢ (i \in ℂ \land 1 \in ℂ) \to i + 1 - 1 = i$
71	68 69 70	sylancl	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to i + 1 - 1 = i$
72	71	fveq2d	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F (i + 1 - 1) = F (i)$
73	72	fveq2d	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to T (F (i + 1 - 1)) = T (F (i))$
74	73	rneqd	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to ran T (F (i + 1 - 1)) = ran T (F (i))$
75	66 74	eleqtrd	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F (i + 1) \in ran T (F (i))$
76	1 2 3 4	efgi2	$⊢ (F (i) \in W \land F (i + 1) \in ran T (F (i))) \to F (i) \underset{˙}{\sim} F (i + 1)$
77	51 75 76	syl2anc	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to F (i) \underset{˙}{\sim} F (i + 1)$
78	36	a1i	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to \underset{˙}{\sim} Er W$
79	78	ertr	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to ((F (0) \underset{˙}{\sim} F (i) \land F (i) \underset{˙}{\sim} F (i + 1)) \to F (0) \underset{˙}{\sim} F (i + 1))$
80	77 79	mpan2d	$⊢ (F \in dom S \land i \in ℕ_{0} \land i + 1 \in (0 ..^\|F\|)) \to (F (0) \underset{˙}{\sim} F (i) \to F (0) \underset{˙}{\sim} F (i + 1))$
81	80	3expia	$⊢ (F \in dom S \land i \in ℕ_{0}) \to (i + 1 \in (0 ..^\|F\|) \to (F (0) \underset{˙}{\sim} F (i) \to F (0) \underset{˙}{\sim} F (i + 1)))$
82	81	a2d	$⊢ (F \in dom S \land i \in ℕ_{0}) \to ((i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)) \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1)))$
83	49 82	syld	$⊢ (F \in dom S \land i \in ℕ_{0}) \to ((i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)) \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1)))$
84	83	expcom	$⊢ i \in ℕ_{0} \to (F \in dom S \to ((i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i)) \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1))))$
85	84	a2d	$⊢ i \in ℕ_{0} \to ((F \in dom S \to (i \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i))) \to (F \in dom S \to (i + 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (i + 1))))$
86	20 25 30 35 43 85	nn0ind	$⊢ \|F\| - 1 \in ℕ_{0} \to (F \in dom S \to (\|F\| - 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (\|F\| - 1)))$
87	15 86	mpcom	$⊢ F \in dom S \to (\|F\| - 1 \in (0 ..^\|F\|) \to F (0) \underset{˙}{\sim} F (\|F\| - 1))$
88	13 87	mpd	$⊢ F \in dom S \to F (0) \underset{˙}{\sim} F (\|F\| - 1)$
89	1 2 3 4 5 6	efgsval	$⊢ F \in dom S \to S (F) = F (\|F\| - 1)$
90	88 89	breqtrrd	$⊢ F \in dom S \to F (0) \underset{˙}{\sim} S (F)$

Metamath Proof Explorer

Theorem efgsrel

Proof