# Metamath Proof Explorer

## Theorem frgpinv

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

Ref Expression
`|- W = ( _I ` Word ( I X. 2o ) )`
`|- G = ( freeGrp ` I )`
`|- .~ = ( ~FG ` I )`
frgpinv.n
`|- N = ( invg ` G )`
frgpinv.m
`|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )`
Assertion frgpinv
`|- ( A e. W -> ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ )`

### Proof

Step Hyp Ref Expression
` |-  W = ( _I ` Word ( I X. 2o ) )`
` |-  G = ( freeGrp ` I )`
` |-  .~ = ( ~FG ` I )`
4 frgpinv.n
` |-  N = ( invg ` G )`
5 frgpinv.m
` |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )`
6 fviss
` |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )`
7 1 6 eqsstri
` |-  W C_ Word ( I X. 2o )`
8 7 sseli
` |-  ( A e. W -> A e. Word ( I X. 2o ) )`
9 revcl
` |-  ( A e. Word ( I X. 2o ) -> ( reverse ` A ) e. Word ( I X. 2o ) )`
10 8 9 syl
` |-  ( A e. W -> ( reverse ` A ) e. Word ( I X. 2o ) )`
11 5 efgmf
` |-  M : ( I X. 2o ) --> ( I X. 2o )`
12 wrdco
` |-  ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )`
13 10 11 12 sylancl
` |-  ( A e. W -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )`
14 1 efgrcl
` |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )`
15 14 simprd
` |-  ( A e. W -> W = Word ( I X. 2o ) )`
16 13 15 eleqtrrd
` |-  ( A e. W -> ( M o. ( reverse ` A ) ) e. W )`
17 eqid
` |-  ( +g ` G ) = ( +g ` G )`
18 1 2 3 17 frgpadd
` |-  ( ( A e. W /\ ( M o. ( reverse ` A ) ) e. W ) -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ )`
19 16 18 mpdan
` |-  ( A e. W -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ )`
20 1 3 efger
` |-  .~ Er W`
21 20 a1i
` |-  ( A e. W -> .~ Er W )`
22 eqid
` |-  ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )`
23 1 3 5 22 efginvrel2
` |-  ( A e. W -> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) )`
24 21 23 erthi
` |-  ( A e. W -> [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ = [ (/) ] .~ )`
25 2 3 frgp0
` |-  ( I e. _V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )`
` |-  ( ( I e. _V /\ W = Word ( I X. 2o ) ) -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )`
27 14 26 syl
` |-  ( A e. W -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )`
28 27 simprd
` |-  ( A e. W -> [ (/) ] .~ = ( 0g ` G ) )`
29 19 24 28 3eqtrd
` |-  ( A e. W -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) )`
30 27 simpld
` |-  ( A e. W -> G e. Grp )`
31 eqid
` |-  ( Base ` G ) = ( Base ` G )`
32 2 3 1 31 frgpeccl
` |-  ( A e. W -> [ A ] .~ e. ( Base ` G ) )`
33 2 3 1 31 frgpeccl
` |-  ( ( M o. ( reverse ` A ) ) e. W -> [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) )`
34 16 33 syl
` |-  ( A e. W -> [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) )`
35 eqid
` |-  ( 0g ` G ) = ( 0g ` G )`
36 31 17 35 4 grpinvid1
` |-  ( ( G e. Grp /\ [ A ] .~ e. ( Base ` G ) /\ [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) ) -> ( ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ <-> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) ) )`
37 30 32 34 36 syl3anc
` |-  ( A e. W -> ( ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ <-> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) ) )`
38 29 37 mpbird
` |-  ( A e. W -> ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ )`