Metamath Proof Explorer


Theorem 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 × 2 𝑜
efgval.r ˙ = ~ FG I
efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
efgred.d D = W x W ran T x
efgred.s S = m t Word W | t 0 D k 1 ..^ t t k ran T t k 1 m m 1
efgrelexlem.1 L = i j | c S -1 i d S -1 j c 0 = d 0
Assertion efgrelexlemb ˙ L

Proof

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