efgrelexlemb

Description: If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A , b ends at B , and a and B have the same starting point. (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))$
	efgrelexlem.1	$⊢ L = \{⟨i, j⟩ \| \exists c \in S^{-1} [\{i\}] \exists d \in S^{-1} [\{j\}] c (0) = d (0)\}$
Assertion	efgrelexlemb	$⊢ \underset{˙}{\sim} \subseteq L$

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		efgrelexlem.1	$⊢ L = \{⟨i, j⟩ \| \exists c \in S^{-1} [\{i\}] \exists d \in S^{-1} [\{j\}] c (0) = d (0)\}$
8	1 2 3 4	efgval2	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\}$
9	7	relopabiv	$⊢ Rel L$
10	9	a1i	$⊢ ⊤ \to Rel L$
11		simpr	$⊢ (⊤ \land f L g) \to f L g$
12		eqcom	$⊢ a (0) = b (0) \leftrightarrow b (0) = a (0)$
13	12	2rexbii	$⊢ \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] a (0) = b (0) \leftrightarrow \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] b (0) = a (0)$
14		rexcom	$⊢ \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] b (0) = a (0) \leftrightarrow \exists b \in S^{-1} [\{g\}] \exists a \in S^{-1} [\{f\}] b (0) = a (0)$
15	13 14	bitri	$⊢ \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] a (0) = b (0) \leftrightarrow \exists b \in S^{-1} [\{g\}] \exists a \in S^{-1} [\{f\}] b (0) = a (0)$
16	1 2 3 4 5 6 7	efgrelexlema	$⊢ f L g \leftrightarrow \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] a (0) = b (0)$
17	1 2 3 4 5 6 7	efgrelexlema	$⊢ g L f \leftrightarrow \exists b \in S^{-1} [\{g\}] \exists a \in S^{-1} [\{f\}] b (0) = a (0)$
18	15 16 17	3bitr4i	$⊢ f L g \leftrightarrow g L f$
19	11 18	sylib	$⊢ (⊤ \land f L g) \to g L f$
20	1 2 3 4 5 6 7	efgrelexlema	$⊢ g L h \leftrightarrow \exists r \in S^{-1} [\{g\}] \exists s \in S^{-1} [\{h\}] r (0) = s (0)$
21		reeanv	$⊢ \exists a \in S^{-1} [\{f\}] \exists r \in S^{-1} [\{g\}] (\exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists s \in S^{-1} [\{h\}] r (0) = s (0)) \leftrightarrow (\exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists r \in S^{-1} [\{g\}] \exists s \in S^{-1} [\{h\}] r (0) = s (0))$
22	1 2 3 4 5 6	efgsfo	$⊢ S : dom S \underset{onto}{⟶} W$
23		fofn	$⊢ S : dom S \underset{onto}{⟶} W \to S Fn dom S$
24	22 23	ax-mp	$⊢ S Fn dom S$
25		fniniseg	$⊢ S Fn dom S \to (r \in S^{-1} [\{g\}] \leftrightarrow (r \in dom S \land S (r) = g))$
26	24 25	ax-mp	$⊢ r \in S^{-1} [\{g\}] \leftrightarrow (r \in dom S \land S (r) = g)$
27		fniniseg	$⊢ S Fn dom S \to (b \in S^{-1} [\{g\}] \leftrightarrow (b \in dom S \land S (b) = g))$
28	24 27	ax-mp	$⊢ b \in S^{-1} [\{g\}] \leftrightarrow (b \in dom S \land S (b) = g)$
29		eqtr3	$⊢ (S (r) = g \land S (b) = g) \to S (r) = S (b)$
30	1 2 3 4 5 6	efgred	$⊢ (r \in dom S \land b \in dom S \land S (r) = S (b)) \to r (0) = b (0)$
31	30	eqcomd	$⊢ (r \in dom S \land b \in dom S \land S (r) = S (b)) \to b (0) = r (0)$
32	31	3expa	$⊢ ((r \in dom S \land b \in dom S) \land S (r) = S (b)) \to b (0) = r (0)$
33	29 32	sylan2	$⊢ ((r \in dom S \land b \in dom S) \land (S (r) = g \land S (b) = g)) \to b (0) = r (0)$
34	33	an4s	$⊢ ((r \in dom S \land S (r) = g) \land (b \in dom S \land S (b) = g)) \to b (0) = r (0)$
35	26 28 34	syl2anb	$⊢ (r \in S^{-1} [\{g\}] \land b \in S^{-1} [\{g\}]) \to b (0) = r (0)$
36		eqeq2	$⊢ r (0) = s (0) \to (b (0) = r (0) \leftrightarrow b (0) = s (0))$
37	35 36	syl5ibcom	$⊢ (r \in S^{-1} [\{g\}] \land b \in S^{-1} [\{g\}]) \to (r (0) = s (0) \to b (0) = s (0))$
38	37	reximdv	$⊢ (r \in S^{-1} [\{g\}] \land b \in S^{-1} [\{g\}]) \to (\exists s \in S^{-1} [\{h\}] r (0) = s (0) \to \exists s \in S^{-1} [\{h\}] b (0) = s (0))$
39		eqeq1	$⊢ a (0) = b (0) \to (a (0) = s (0) \leftrightarrow b (0) = s (0))$
40	39	rexbidv	$⊢ a (0) = b (0) \to (\exists s \in S^{-1} [\{h\}] a (0) = s (0) \leftrightarrow \exists s \in S^{-1} [\{h\}] b (0) = s (0))$
41	40	imbi2d	$⊢ a (0) = b (0) \to ((\exists s \in S^{-1} [\{h\}] r (0) = s (0) \to \exists s \in S^{-1} [\{h\}] a (0) = s (0)) \leftrightarrow (\exists s \in S^{-1} [\{h\}] r (0) = s (0) \to \exists s \in S^{-1} [\{h\}] b (0) = s (0)))$
42	38 41	syl5ibrcom	$⊢ (r \in S^{-1} [\{g\}] \land b \in S^{-1} [\{g\}]) \to (a (0) = b (0) \to (\exists s \in S^{-1} [\{h\}] r (0) = s (0) \to \exists s \in S^{-1} [\{h\}] a (0) = s (0)))$
43	42	rexlimdva	$⊢ r \in S^{-1} [\{g\}] \to (\exists b \in S^{-1} [\{g\}] a (0) = b (0) \to (\exists s \in S^{-1} [\{h\}] r (0) = s (0) \to \exists s \in S^{-1} [\{h\}] a (0) = s (0)))$
44	43	impd	$⊢ r \in S^{-1} [\{g\}] \to ((\exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists s \in S^{-1} [\{h\}] r (0) = s (0)) \to \exists s \in S^{-1} [\{h\}] a (0) = s (0))$
45	44	rexlimiv	$⊢ \exists r \in S^{-1} [\{g\}] (\exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists s \in S^{-1} [\{h\}] r (0) = s (0)) \to \exists s \in S^{-1} [\{h\}] a (0) = s (0)$
46	45	reximi	$⊢ \exists a \in S^{-1} [\{f\}] \exists r \in S^{-1} [\{g\}] (\exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists s \in S^{-1} [\{h\}] r (0) = s (0)) \to \exists a \in S^{-1} [\{f\}] \exists s \in S^{-1} [\{h\}] a (0) = s (0)$
47	21 46	sylbir	$⊢ (\exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{g\}] a (0) = b (0) \land \exists r \in S^{-1} [\{g\}] \exists s \in S^{-1} [\{h\}] r (0) = s (0)) \to \exists a \in S^{-1} [\{f\}] \exists s \in S^{-1} [\{h\}] a (0) = s (0)$
48	16 20 47	syl2anb	$⊢ (f L g \land g L h) \to \exists a \in S^{-1} [\{f\}] \exists s \in S^{-1} [\{h\}] a (0) = s (0)$
49	1 2 3 4 5 6 7	efgrelexlema	$⊢ f L h \leftrightarrow \exists a \in S^{-1} [\{f\}] \exists s \in S^{-1} [\{h\}] a (0) = s (0)$
50	48 49	sylibr	$⊢ (f L g \land g L h) \to f L h$
51	50	adantl	$⊢ (⊤ \land (f L g \land g L h)) \to f L h$
52		eqid	$⊢ a (0) = a (0)$
53		fveq1	$⊢ b = a \to b (0) = a (0)$
54	53	rspceeqv	$⊢ (a \in S^{-1} [\{f\}] \land a (0) = a (0)) \to \exists b \in S^{-1} [\{f\}] a (0) = b (0)$
55	52 54	mpan2	$⊢ a \in S^{-1} [\{f\}] \to \exists b \in S^{-1} [\{f\}] a (0) = b (0)$
56	55	pm4.71i	$⊢ a \in S^{-1} [\{f\}] \leftrightarrow (a \in S^{-1} [\{f\}] \land \exists b \in S^{-1} [\{f\}] a (0) = b (0))$
57		fniniseg	$⊢ S Fn dom S \to (a \in S^{-1} [\{f\}] \leftrightarrow (a \in dom S \land S (a) = f))$
58	24 57	ax-mp	$⊢ a \in S^{-1} [\{f\}] \leftrightarrow (a \in dom S \land S (a) = f)$
59	56 58	bitr3i	$⊢ (a \in S^{-1} [\{f\}] \land \exists b \in S^{-1} [\{f\}] a (0) = b (0)) \leftrightarrow (a \in dom S \land S (a) = f)$
60	59	rexbii2	$⊢ \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{f\}] a (0) = b (0) \leftrightarrow \exists a \in dom S S (a) = f$
61	1 2 3 4 5 6 7	efgrelexlema	$⊢ f L f \leftrightarrow \exists a \in S^{-1} [\{f\}] \exists b \in S^{-1} [\{f\}] a (0) = b (0)$
62		forn	$⊢ S : dom S \underset{onto}{⟶} W \to ran S = W$
63	22 62	ax-mp	$⊢ ran S = W$
64	63	eleq2i	$⊢ f \in ran S \leftrightarrow f \in W$
65		fvelrnb	$⊢ S Fn dom S \to (f \in ran S \leftrightarrow \exists a \in dom S S (a) = f)$
66	24 65	ax-mp	$⊢ f \in ran S \leftrightarrow \exists a \in dom S S (a) = f$
67	64 66	bitr3i	$⊢ f \in W \leftrightarrow \exists a \in dom S S (a) = f$
68	60 61 67	3bitr4ri	$⊢ f \in W \leftrightarrow f L f$
69	68	a1i	$⊢ ⊤ \to (f \in W \leftrightarrow f L f)$
70	10 19 51 69	iserd	$⊢ ⊤ \to L Er W$
71	70	mptru	$⊢ L Er W$
72		simpl	$⊢ (a \in W \land b \in ran T (a)) \to a \in W$
73		foelrn	$⊢ (S : dom S \underset{onto}{⟶} W \land a \in W) \to \exists r \in dom S a = S (r)$
74	22 72 73	sylancr	$⊢ (a \in W \land b \in ran T (a)) \to \exists r \in dom S a = S (r)$
75		simprl	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r \in dom S$
76		simprr	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to a = S (r)$
77	76	eqcomd	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to S (r) = a$
78		fniniseg	$⊢ S Fn dom S \to (r \in S^{-1} [\{a\}] \leftrightarrow (r \in dom S \land S (r) = a))$
79	24 78	ax-mp	$⊢ r \in S^{-1} [\{a\}] \leftrightarrow (r \in dom S \land S (r) = a)$
80	75 77 79	sylanbrc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r \in S^{-1} [\{a\}]$
81		simplr	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to b \in ran T (a)$
82	76	fveq2d	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to T (a) = T (S (r))$
83	82	rneqd	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to ran T (a) = ran T (S (r))$
84	81 83	eleqtrd	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to b \in ran T (S (r))$
85	1 2 3 4 5 6	efgsp1	$⊢ (r \in dom S \land b \in ran T (S (r))) \to r ++ ⟨“ b ”⟩ \in dom S$
86	75 84 85	syl2anc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r ++ ⟨“ b ”⟩ \in dom S$
87	1 2 3 4 5 6	efgsdm	$⊢ r \in dom S \leftrightarrow (r \in (Word W ∖ \{\emptyset\}) \land r (0) \in D \land \forall i \in (1 ..^\|r\|) r (i) \in ran T (r (i - 1)))$
88	87	simp1bi	$⊢ r \in dom S \to r \in (Word W ∖ \{\emptyset\})$
89	88	ad2antrl	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r \in (Word W ∖ \{\emptyset\})$
90	89	eldifad	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r \in Word W$
91	1 2 3 4	efgtf	$⊢ a \in W \to (T (a) = (f \in (0 \dots \|a\|), g \in (I \times 2_{𝑜}) ⟼ a splice ⟨f, f, ⟨“ g M (g) ”⟩⟩) \land T (a) : (0 \dots \|a\|) \times (I \times 2_{𝑜}) ⟶ W)$
92	91	simprd	$⊢ a \in W \to T (a) : (0 \dots \|a\|) \times (I \times 2_{𝑜}) ⟶ W$
93	92	frnd	$⊢ a \in W \to ran T (a) \subseteq W$
94	93	sselda	$⊢ (a \in W \land b \in ran T (a)) \to b \in W$
95	94	adantr	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to b \in W$
96	1 2 3 4 5 6	efgsval2	$⊢ (r \in Word W \land b \in W \land r ++ ⟨“ b ”⟩ \in dom S) \to S (r ++ ⟨“ b ”⟩) = b$
97	90 95 86 96	syl3anc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to S (r ++ ⟨“ b ”⟩) = b$
98		fniniseg	$⊢ S Fn dom S \to (r ++ ⟨“ b ”⟩ \in S^{-1} [\{b\}] \leftrightarrow (r ++ ⟨“ b ”⟩ \in dom S \land S (r ++ ⟨“ b ”⟩) = b))$
99	24 98	ax-mp	$⊢ r ++ ⟨“ b ”⟩ \in S^{-1} [\{b\}] \leftrightarrow (r ++ ⟨“ b ”⟩ \in dom S \land S (r ++ ⟨“ b ”⟩) = b)$
100	86 97 99	sylanbrc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r ++ ⟨“ b ”⟩ \in S^{-1} [\{b\}]$
101	95	s1cld	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to ⟨“ b ”⟩ \in Word W$
102		eldifsn	$⊢ r \in (Word W ∖ \{\emptyset\}) \leftrightarrow (r \in Word W \land r \neq \emptyset)$
103		lennncl	$⊢ (r \in Word W \land r \neq \emptyset) \to \|r\| \in ℕ$
104	102 103	sylbi	$⊢ r \in (Word W ∖ \{\emptyset\}) \to \|r\| \in ℕ$
105	89 104	syl	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to \|r\| \in ℕ$
106		lbfzo0	$⊢ 0 \in (0 ..^\|r\|) \leftrightarrow \|r\| \in ℕ$
107	105 106	sylibr	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to 0 \in (0 ..^\|r\|)$
108		ccatval1	$⊢ (r \in Word W \land ⟨“ b ”⟩ \in Word W \land 0 \in (0 ..^\|r\|)) \to (r ++ ⟨“ b ”⟩) (0) = r (0)$
109	90 101 107 108	syl3anc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to (r ++ ⟨“ b ”⟩) (0) = r (0)$
110	109	eqcomd	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to r (0) = (r ++ ⟨“ b ”⟩) (0)$
111		fveq1	$⊢ s = r ++ ⟨“ b ”⟩ \to s (0) = (r ++ ⟨“ b ”⟩) (0)$
112	111	rspceeqv	$⊢ (r ++ ⟨“ b ”⟩ \in S^{-1} [\{b\}] \land r (0) = (r ++ ⟨“ b ”⟩) (0)) \to \exists s \in S^{-1} [\{b\}] r (0) = s (0)$
113	100 110 112	syl2anc	$⊢ ((a \in W \land b \in ran T (a)) \land (r \in dom S \land a = S (r))) \to \exists s \in S^{-1} [\{b\}] r (0) = s (0)$
114	74 80 113	reximssdv	$⊢ (a \in W \land b \in ran T (a)) \to \exists r \in S^{-1} [\{a\}] \exists s \in S^{-1} [\{b\}] r (0) = s (0)$
115	1 2 3 4 5 6 7	efgrelexlema	$⊢ a L b \leftrightarrow \exists r \in S^{-1} [\{a\}] \exists s \in S^{-1} [\{b\}] r (0) = s (0)$
116	114 115	sylibr	$⊢ (a \in W \land b \in ran T (a)) \to a L b$
117		vex	$⊢ b \in V$
118		vex	$⊢ a \in V$
119	117 118	elec	$⊢ b \in [a] L \leftrightarrow a L b$
120	116 119	sylibr	$⊢ (a \in W \land b \in ran T (a)) \to b \in [a] L$
121	120	ex	$⊢ a \in W \to (b \in ran T (a) \to b \in [a] L)$
122	121	ssrdv	$⊢ a \in W \to ran T (a) \subseteq [a] L$
123	122	rgen	$⊢ \forall a \in W ran T (a) \subseteq [a] L$
124	1	fvexi	$⊢ W \in V$
125		erex	$⊢ L Er W \to (W \in V \to L \in V)$
126	71 124 125	mp2	$⊢ L \in V$
127		ereq1	$⊢ r = L \to (r Er W \leftrightarrow L Er W)$
128		eceq2	$⊢ r = L \to [a] r = [a] L$
129	128	sseq2d	$⊢ r = L \to (ran T (a) \subseteq [a] r \leftrightarrow ran T (a) \subseteq [a] L)$
130	129	ralbidv	$⊢ r = L \to (\forall a \in W ran T (a) \subseteq [a] r \leftrightarrow \forall a \in W ran T (a) \subseteq [a] L)$
131	127 130	anbi12d	$⊢ r = L \to ((r Er W \land \forall a \in W ran T (a) \subseteq [a] r) \leftrightarrow (L Er W \land \forall a \in W ran T (a) \subseteq [a] L))$
132	126 131	elab	$⊢ L \in \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\} \leftrightarrow (L Er W \land \forall a \in W ran T (a) \subseteq [a] L)$
133	71 123 132	mpbir2an	$⊢ L \in \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\}$
134		intss1	$⊢ L \in \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\} \to ⋂ \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\} \subseteq L$
135	133 134	ax-mp	$⊢ ⋂ \{r \| (r Er W \land \forall a \in W ran T (a) \subseteq [a] r)\} \subseteq L$
136	8 135	eqsstri	$⊢ \underset{˙}{\sim} \subseteq L$

Metamath Proof Explorer

Theorem efgrelexlemb

Proof