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

Metamath Proof Explorer

Theorem efgrelexlemb

Proof