# Metamath Proof Explorer

## Theorem frgpinv

Description: The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses frgpadd.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
frgpadd.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
frgpinv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
frgpinv.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
Assertion frgpinv

### Proof

Step Hyp Ref Expression
1 frgpadd.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 frgpadd.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
4 frgpinv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
5 frgpinv.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
6 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
7 1 6 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
8 7 sseli ${⊢}{A}\in {W}\to {A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
9 revcl ${⊢}{A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \mathrm{reverse}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
10 8 9 syl ${⊢}{A}\in {W}\to \mathrm{reverse}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
11 5 efgmf ${⊢}{M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$
12 wrdco ${⊢}\left(\mathrm{reverse}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}\right)\to {M}\circ \mathrm{reverse}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
13 10 11 12 sylancl ${⊢}{A}\in {W}\to {M}\circ \mathrm{reverse}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
14 1 efgrcl ${⊢}{A}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
15 14 simprd ${⊢}{A}\in {W}\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
16 13 15 eleqtrrd ${⊢}{A}\in {W}\to {M}\circ \mathrm{reverse}\left({A}\right)\in {W}$
17 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
18 1 2 3 17 frgpadd
19 16 18 mpdan
20 1 3 efger
21 20 a1i
22 eqid ${⊢}\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
23 1 3 5 22 efginvrel2
24 21 23 erthi
25 2 3 frgp0
30 27 simpld ${⊢}{A}\in {W}\to {G}\in \mathrm{Grp}$
31 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
35 eqid ${⊢}{0}_{{G}}={0}_{{G}}$