Metamath Proof Explorer

Theorem efginvrel1

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 efginvrel1 ⊢ A ∈ W → M ∘ reverse ⁡ A ++ 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 revcl ⊢ A ∈ Word I × 2 𝑜 → reverse ⁡ A ∈ Word I × 2 𝑜
9 7 8 syl ⊢ A ∈ W → reverse ⁡ A ∈ Word I × 2 𝑜
10 3 efgmf ⊢ M : I × 2 𝑜 ⟶ I × 2 𝑜
11 revco ⊢ reverse ⁡ A ∈ Word I × 2 𝑜 ∧ M : I × 2 𝑜 ⟶ I × 2 𝑜 → M ∘ reverse ⁡ reverse ⁡ A = reverse ⁡ M ∘ reverse ⁡ A
12 9 10 11 sylancl ⊢ A ∈ W → M ∘ reverse ⁡ reverse ⁡ A = reverse ⁡ M ∘ reverse ⁡ A
13 revrev ⊢ A ∈ Word I × 2 𝑜 → reverse ⁡ reverse ⁡ A = A
14 7 13 syl ⊢ A ∈ W → reverse ⁡ reverse ⁡ A = A
15 14 coeq2d ⊢ A ∈ W → M ∘ reverse ⁡ reverse ⁡ A = M ∘ A
16 12 15 eqtr3d ⊢ A ∈ W → reverse ⁡ M ∘ reverse ⁡ A = M ∘ A
17 16 coeq2d ⊢ A ∈ W → M ∘ reverse ⁡ M ∘ reverse ⁡ A = M ∘ M ∘ A
18 wrdf ⊢ A ∈ Word I × 2 𝑜 → A : 0 ..^ A ⟶ I × 2 𝑜
19 7 18 syl ⊢ A ∈ W → A : 0 ..^ A ⟶ I × 2 𝑜
20 19 ffvelrnda ⊢ A ∈ W ∧ c ∈ 0 ..^ A → A ⁡ c ∈ I × 2 𝑜
21 3 efgmnvl ⊢ A ⁡ c ∈ I × 2 𝑜 → M ⁡ M ⁡ A ⁡ c = A ⁡ c
22 20 21 syl ⊢ A ∈ W ∧ c ∈ 0 ..^ A → M ⁡ M ⁡ A ⁡ c = A ⁡ c
23 22 mpteq2dva ⊢ A ∈ W → c ∈ 0 ..^ A ⟼ M ⁡ M ⁡ A ⁡ c = c ∈ 0 ..^ A ⟼ A ⁡ c
24 10 ffvelrni ⊢ A ⁡ c ∈ I × 2 𝑜 → M ⁡ A ⁡ c ∈ I × 2 𝑜
25 20 24 syl ⊢ A ∈ W ∧ c ∈ 0 ..^ A → M ⁡ A ⁡ c ∈ I × 2 𝑜
26 fcompt ⊢ M : I × 2 𝑜 ⟶ I × 2 𝑜 ∧ A : 0 ..^ A ⟶ I × 2 𝑜 → M ∘ A = c ∈ 0 ..^ A ⟼ M ⁡ A ⁡ c
27 10 19 26 sylancr ⊢ A ∈ W → M ∘ A = c ∈ 0 ..^ A ⟼ M ⁡ A ⁡ c
28 10 a1i ⊢ A ∈ W → M : I × 2 𝑜 ⟶ I × 2 𝑜
29 28 feqmptd ⊢ A ∈ W → M = a ∈ I × 2 𝑜 ⟼ M ⁡ a
30 fveq2 ⊢ a = M ⁡ A ⁡ c → M ⁡ a = M ⁡ M ⁡ A ⁡ c
31 25 27 29 30 fmptco ⊢ A ∈ W → M ∘ M ∘ A = c ∈ 0 ..^ A ⟼ M ⁡ M ⁡ A ⁡ c
32 19 feqmptd ⊢ A ∈ W → A = c ∈ 0 ..^ A ⟼ A ⁡ c
33 23 31 32 3eqtr4d ⊢ A ∈ W → M ∘ M ∘ A = A
34 17 33 eqtrd ⊢ A ∈ W → M ∘ reverse ⁡ M ∘ reverse ⁡ A = A
35 34 oveq2d ⊢ A ∈ W → M ∘ reverse ⁡ A ++ M ∘ reverse ⁡ M ∘ reverse ⁡ A = M ∘ reverse ⁡ A ++ A
36 wrdco ⊢ reverse ⁡ A ∈ Word I × 2 𝑜 ∧ M : I × 2 𝑜 ⟶ I × 2 𝑜 → M ∘ reverse ⁡ A ∈ Word I × 2 𝑜
37 9 10 36 sylancl ⊢ A ∈ W → M ∘ reverse ⁡ A ∈ Word I × 2 𝑜
38 1 efgrcl ⊢ A ∈ W → I ∈ V ∧ W = Word I × 2 𝑜
39 38 simprd ⊢ A ∈ W → W = Word I × 2 𝑜
40 37 39 eleqtrrd ⊢ A ∈ W → M ∘ reverse ⁡ A ∈ W
41 1 2 3 4 efginvrel2 ⊢ M ∘ reverse ⁡ A ∈ W → M ∘ reverse ⁡ A ++ M ∘ reverse ⁡ M ∘ reverse ⁡ A ∼ ˙ ∅
42 40 41 syl ⊢ A ∈ W → M ∘ reverse ⁡ A ++ M ∘ reverse ⁡ M ∘ reverse ⁡ A ∼ ˙ ∅
43 35 42 eqbrtrrd ⊢ A ∈ W → M ∘ reverse ⁡ A ++ A ∼ ˙ ∅