Metamath Proof Explorer


Theorem efginvrel2

Description: The inverse of the reverse of a word composed with the word relates to the identity. (This provides an explicit expression for the representation of the group inverse, given a representative of the free group equivalence class.) (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 ”⟩
Assertion efginvrel2 A W A ++ M reverse A ˙

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 fviss I Word I × 2 𝑜 Word I × 2 𝑜
6 1 5 eqsstri W Word I × 2 𝑜
7 6 sseli A W A Word I × 2 𝑜
8 id c = c =
9 fveq2 c = reverse c = reverse
10 rev0 reverse =
11 9 10 eqtrdi c = reverse c =
12 11 coeq2d c = M reverse c = M
13 co02 M =
14 12 13 eqtrdi c = M reverse c =
15 8 14 oveq12d c = c ++ M reverse c = ++
16 15 breq1d c = c ++ M reverse c ˙ ++ ˙
17 16 imbi2d c = A W c ++ M reverse c ˙ A W ++ ˙
18 id c = a c = a
19 fveq2 c = a reverse c = reverse a
20 19 coeq2d c = a M reverse c = M reverse a
21 18 20 oveq12d c = a c ++ M reverse c = a ++ M reverse a
22 21 breq1d c = a c ++ M reverse c ˙ a ++ M reverse a ˙
23 22 imbi2d c = a A W c ++ M reverse c ˙ A W a ++ M reverse a ˙
24 id c = a ++ ⟨“ b ”⟩ c = a ++ ⟨“ b ”⟩
25 fveq2 c = a ++ ⟨“ b ”⟩ reverse c = reverse a ++ ⟨“ b ”⟩
26 25 coeq2d c = a ++ ⟨“ b ”⟩ M reverse c = M reverse a ++ ⟨“ b ”⟩
27 24 26 oveq12d c = a ++ ⟨“ b ”⟩ c ++ M reverse c = a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩
28 27 breq1d c = a ++ ⟨“ b ”⟩ c ++ M reverse c ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
29 28 imbi2d c = a ++ ⟨“ b ”⟩ A W c ++ M reverse c ˙ A W a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
30 id c = A c = A
31 fveq2 c = A reverse c = reverse A
32 31 coeq2d c = A M reverse c = M reverse A
33 30 32 oveq12d c = A c ++ M reverse c = A ++ M reverse A
34 33 breq1d c = A c ++ M reverse c ˙ A ++ M reverse A ˙
35 34 imbi2d c = A A W c ++ M reverse c ˙ A W A ++ M reverse A ˙
36 ccatidid ++ =
37 1 2 efger ˙ Er W
38 37 a1i A W ˙ Er W
39 wrd0 Word I × 2 𝑜
40 1 efgrcl A W I V W = Word I × 2 𝑜
41 40 simprd A W W = Word I × 2 𝑜
42 39 41 eleqtrrid A W W
43 38 42 erref A W ˙
44 36 43 eqbrtrid A W ++ ˙
45 37 a1i A W a Word I × 2 𝑜 b I × 2 𝑜 ˙ Er W
46 simprl A W a Word I × 2 𝑜 b I × 2 𝑜 a Word I × 2 𝑜
47 revcl a Word I × 2 𝑜 reverse a Word I × 2 𝑜
48 47 ad2antrl A W a Word I × 2 𝑜 b I × 2 𝑜 reverse a Word I × 2 𝑜
49 3 efgmf M : I × 2 𝑜 I × 2 𝑜
50 wrdco reverse a Word I × 2 𝑜 M : I × 2 𝑜 I × 2 𝑜 M reverse a Word I × 2 𝑜
51 48 49 50 sylancl A W a Word I × 2 𝑜 b I × 2 𝑜 M reverse a Word I × 2 𝑜
52 ccatcl a Word I × 2 𝑜 M reverse a Word I × 2 𝑜 a ++ M reverse a Word I × 2 𝑜
53 46 51 52 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a Word I × 2 𝑜
54 41 adantr A W a Word I × 2 𝑜 b I × 2 𝑜 W = Word I × 2 𝑜
55 53 54 eleqtrrd A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a W
56 lencl a Word I × 2 𝑜 a 0
57 56 ad2antrl A W a Word I × 2 𝑜 b I × 2 𝑜 a 0
58 nn0uz 0 = 0
59 57 58 eleqtrdi A W a Word I × 2 𝑜 b I × 2 𝑜 a 0
60 ccatlen a Word I × 2 𝑜 M reverse a Word I × 2 𝑜 a ++ M reverse a = a + M reverse a
61 46 51 60 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a = a + M reverse a
62 57 nn0zd A W a Word I × 2 𝑜 b I × 2 𝑜 a
63 62 uzidd A W a Word I × 2 𝑜 b I × 2 𝑜 a a
64 lencl M reverse a Word I × 2 𝑜 M reverse a 0
65 51 64 syl A W a Word I × 2 𝑜 b I × 2 𝑜 M reverse a 0
66 uzaddcl a a M reverse a 0 a + M reverse a a
67 63 65 66 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 a + M reverse a a
68 61 67 eqeltrd A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a a
69 elfzuzb a 0 a ++ M reverse a a 0 a ++ M reverse a a
70 59 68 69 sylanbrc A W a Word I × 2 𝑜 b I × 2 𝑜 a 0 a ++ M reverse a
71 simprr A W a Word I × 2 𝑜 b I × 2 𝑜 b I × 2 𝑜
72 1 2 3 4 efgtval a ++ M reverse a W a 0 a ++ M reverse a b I × 2 𝑜 a T a ++ M reverse a b = a ++ M reverse a splice a a ⟨“ b M b ”⟩
73 55 70 71 72 syl3anc A W a Word I × 2 𝑜 b I × 2 𝑜 a T a ++ M reverse a b = a ++ M reverse a splice a a ⟨“ b M b ”⟩
74 39 a1i A W a Word I × 2 𝑜 b I × 2 𝑜 Word I × 2 𝑜
75 49 ffvelrni b I × 2 𝑜 M b I × 2 𝑜
76 75 ad2antll A W a Word I × 2 𝑜 b I × 2 𝑜 M b I × 2 𝑜
77 71 76 s2cld A W a Word I × 2 𝑜 b I × 2 𝑜 ⟨“ b M b ”⟩ Word I × 2 𝑜
78 ccatrid a Word I × 2 𝑜 a ++ = a
79 78 ad2antrl A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ = a
80 79 eqcomd A W a Word I × 2 𝑜 b I × 2 𝑜 a = a ++
81 80 oveq1d A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a = a ++ ++ M reverse a
82 eqidd A W a Word I × 2 𝑜 b I × 2 𝑜 a = a
83 hash0 = 0
84 83 oveq2i a + = a + 0
85 57 nn0cnd A W a Word I × 2 𝑜 b I × 2 𝑜 a
86 85 addid1d A W a Word I × 2 𝑜 b I × 2 𝑜 a + 0 = a
87 84 86 eqtr2id A W a Word I × 2 𝑜 b I × 2 𝑜 a = a +
88 46 74 51 77 81 82 87 splval2 A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a splice a a ⟨“ b M b ”⟩ = a ++ ⟨“ b M b ”⟩ ++ M reverse a
89 71 s1cld A W a Word I × 2 𝑜 b I × 2 𝑜 ⟨“ b ”⟩ Word I × 2 𝑜
90 revccat a Word I × 2 𝑜 ⟨“ b ”⟩ Word I × 2 𝑜 reverse a ++ ⟨“ b ”⟩ = reverse ⟨“ b ”⟩ ++ reverse a
91 46 89 90 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 reverse a ++ ⟨“ b ”⟩ = reverse ⟨“ b ”⟩ ++ reverse a
92 revs1 reverse ⟨“ b ”⟩ = ⟨“ b ”⟩
93 92 oveq1i reverse ⟨“ b ”⟩ ++ reverse a = ⟨“ b ”⟩ ++ reverse a
94 91 93 eqtrdi A W a Word I × 2 𝑜 b I × 2 𝑜 reverse a ++ ⟨“ b ”⟩ = ⟨“ b ”⟩ ++ reverse a
95 94 coeq2d A W a Word I × 2 𝑜 b I × 2 𝑜 M reverse a ++ ⟨“ b ”⟩ = M ⟨“ b ”⟩ ++ reverse a
96 49 a1i A W a Word I × 2 𝑜 b I × 2 𝑜 M : I × 2 𝑜 I × 2 𝑜
97 ccatco ⟨“ b ”⟩ Word I × 2 𝑜 reverse a Word I × 2 𝑜 M : I × 2 𝑜 I × 2 𝑜 M ⟨“ b ”⟩ ++ reverse a = M ⟨“ b ”⟩ ++ M reverse a
98 89 48 96 97 syl3anc A W a Word I × 2 𝑜 b I × 2 𝑜 M ⟨“ b ”⟩ ++ reverse a = M ⟨“ b ”⟩ ++ M reverse a
99 s1co b I × 2 𝑜 M : I × 2 𝑜 I × 2 𝑜 M ⟨“ b ”⟩ = ⟨“ M b ”⟩
100 71 49 99 sylancl A W a Word I × 2 𝑜 b I × 2 𝑜 M ⟨“ b ”⟩ = ⟨“ M b ”⟩
101 100 oveq1d A W a Word I × 2 𝑜 b I × 2 𝑜 M ⟨“ b ”⟩ ++ M reverse a = ⟨“ M b ”⟩ ++ M reverse a
102 95 98 101 3eqtrd A W a Word I × 2 𝑜 b I × 2 𝑜 M reverse a ++ ⟨“ b ”⟩ = ⟨“ M b ”⟩ ++ M reverse a
103 102 oveq2d A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a
104 ccatcl a Word I × 2 𝑜 ⟨“ b ”⟩ Word I × 2 𝑜 a ++ ⟨“ b ”⟩ Word I × 2 𝑜
105 46 89 104 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ Word I × 2 𝑜
106 76 s1cld A W a Word I × 2 𝑜 b I × 2 𝑜 ⟨“ M b ”⟩ Word I × 2 𝑜
107 ccatass a ++ ⟨“ b ”⟩ Word I × 2 𝑜 ⟨“ M b ”⟩ Word I × 2 𝑜 M reverse a Word I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a
108 105 106 51 107 syl3anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a
109 ccatass a Word I × 2 𝑜 ⟨“ b ”⟩ Word I × 2 𝑜 ⟨“ M b ”⟩ Word I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩
110 46 89 106 109 syl3anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩
111 df-s2 ⟨“ b M b ”⟩ = ⟨“ b ”⟩ ++ ⟨“ M b ”⟩
112 111 oveq2i a ++ ⟨“ b M b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩
113 110 112 eqtr4di A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ = a ++ ⟨“ b M b ”⟩
114 113 oveq1d A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ ⟨“ M b ”⟩ ++ M reverse a = a ++ ⟨“ b M b ”⟩ ++ M reverse a
115 103 108 114 3eqtr2rd A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b M b ”⟩ ++ M reverse a = a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩
116 73 88 115 3eqtrd A W a Word I × 2 𝑜 b I × 2 𝑜 a T a ++ M reverse a b = a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩
117 1 2 3 4 efgtf a ++ M reverse a W T a ++ M reverse a = m 0 a ++ M reverse a , u I × 2 𝑜 a ++ M reverse a splice m m ⟨“ u M u ”⟩ T a ++ M reverse a : 0 a ++ M reverse a × I × 2 𝑜 W
118 117 simprd a ++ M reverse a W T a ++ M reverse a : 0 a ++ M reverse a × I × 2 𝑜 W
119 55 118 syl A W a Word I × 2 𝑜 b I × 2 𝑜 T a ++ M reverse a : 0 a ++ M reverse a × I × 2 𝑜 W
120 119 ffnd A W a Word I × 2 𝑜 b I × 2 𝑜 T a ++ M reverse a Fn 0 a ++ M reverse a × I × 2 𝑜
121 fnovrn T a ++ M reverse a Fn 0 a ++ M reverse a × I × 2 𝑜 a 0 a ++ M reverse a b I × 2 𝑜 a T a ++ M reverse a b ran T a ++ M reverse a
122 120 70 71 121 syl3anc A W a Word I × 2 𝑜 b I × 2 𝑜 a T a ++ M reverse a b ran T a ++ M reverse a
123 116 122 eqeltrrd A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ran T a ++ M reverse a
124 1 2 3 4 efgi2 a ++ M reverse a W a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ran T a ++ M reverse a a ++ M reverse a ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩
125 55 123 124 syl2anc A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩
126 45 125 ersym A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙ a ++ M reverse a
127 45 ertr A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙ a ++ M reverse a a ++ M reverse a ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
128 126 127 mpand A W a Word I × 2 𝑜 b I × 2 𝑜 a ++ M reverse a ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
129 128 expcom a Word I × 2 𝑜 b I × 2 𝑜 A W a ++ M reverse a ˙ a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
130 129 a2d a Word I × 2 𝑜 b I × 2 𝑜 A W a ++ M reverse a ˙ A W a ++ ⟨“ b ”⟩ ++ M reverse a ++ ⟨“ b ”⟩ ˙
131 17 23 29 35 44 130 wrdind A Word I × 2 𝑜 A W A ++ M reverse A ˙
132 7 131 mpcom A W A ++ M reverse A ˙