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 = ( _I ` Word ( I X. 2o ) )
frgpadd.g 
|- G = ( freeGrp ` I )
frgpadd.r 
|- .~ = ( ~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
1 frgpadd.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 frgpadd.g 
 |-  G = ( freeGrp ` I )
3 frgpadd.r 
 |-  .~ = ( ~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 ) ) )
26 25 adantr 
 |-  ( ( 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 ) ) ] .~ )