This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
Assertion efginvrel1 
|- ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ A ) .~ (/) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
6 1 5 eqsstri 
 |-  W C_ Word ( I X. 2o )
7 6 sseli 
 |-  ( A e. W -> A e. Word ( I X. 2o ) )
8 revcl 
 |-  ( A e. Word ( I X. 2o ) -> ( reverse ` A ) e. Word ( I X. 2o ) )
9 7 8 syl 
 |-  ( A e. W -> ( reverse ` A ) e. Word ( I X. 2o ) )
10 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
11 revco 
 |-  ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( reverse ` ( M o. ( reverse ` A ) ) ) )
12 9 10 11 sylancl 
 |-  ( A e. W -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( reverse ` ( M o. ( reverse ` A ) ) ) )
13 revrev 
 |-  ( A e. Word ( I X. 2o ) -> ( reverse ` ( reverse ` A ) ) = A )
14 7 13 syl 
 |-  ( A e. W -> ( reverse ` ( reverse ` A ) ) = A )
15 14 coeq2d 
 |-  ( A e. W -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( M o. A ) )
16 12 15 eqtr3d 
 |-  ( A e. W -> ( reverse ` ( M o. ( reverse ` A ) ) ) = ( M o. A ) )
17 16 coeq2d 
 |-  ( A e. W -> ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) = ( M o. ( M o. A ) ) )
18 wrdf 
 |-  ( A e. Word ( I X. 2o ) -> A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) )
19 7 18 syl 
 |-  ( A e. W -> A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) )
20 19 ffvelcdmda 
 |-  ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` c ) e. ( I X. 2o ) )
21 3 efgmnvl 
 |-  ( ( A ` c ) e. ( I X. 2o ) -> ( M ` ( M ` ( A ` c ) ) ) = ( A ` c ) )
22 20 21 syl 
 |-  ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( M ` ( M ` ( A ` c ) ) ) = ( A ` c ) )
23 22 mpteq2dva 
 |-  ( A e. W -> ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( M ` ( A ` c ) ) ) ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( A ` c ) ) )
24 10 ffvelcdmi 
 |-  ( ( A ` c ) e. ( I X. 2o ) -> ( M ` ( A ` c ) ) e. ( I X. 2o ) )
25 20 24 syl 
 |-  ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( M ` ( A ` c ) ) e. ( I X. 2o ) )
26 fcompt 
 |-  ( ( M : ( I X. 2o ) --> ( I X. 2o ) /\ A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) ) -> ( M o. A ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( A ` c ) ) ) )
27 10 19 26 sylancr 
 |-  ( A e. W -> ( M o. A ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( A ` c ) ) ) )
28 10 a1i 
 |-  ( A e. W -> M : ( I X. 2o ) --> ( I X. 2o ) )
29 28 feqmptd 
 |-  ( A e. W -> M = ( a e. ( I X. 2o ) |-> ( M ` a ) ) )
30 fveq2 
 |-  ( a = ( M ` ( A ` c ) ) -> ( M ` a ) = ( M ` ( M ` ( A ` c ) ) ) )
31 25 27 29 30 fmptco 
 |-  ( A e. W -> ( M o. ( M o. A ) ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( M ` ( A ` c ) ) ) ) )
32 19 feqmptd 
 |-  ( A e. W -> A = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( A ` c ) ) )
33 23 31 32 3eqtr4d 
 |-  ( A e. W -> ( M o. ( M o. A ) ) = A )
34 17 33 eqtrd 
 |-  ( A e. W -> ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) = A )
35 34 oveq2d 
 |-  ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) = ( ( M o. ( reverse ` A ) ) ++ A ) )
36 wrdco 
 |-  ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
37 9 10 36 sylancl 
 |-  ( A e. W -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
38 1 efgrcl 
 |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
39 38 simprd 
 |-  ( A e. W -> W = Word ( I X. 2o ) )
40 37 39 eleqtrrd 
 |-  ( A e. W -> ( M o. ( reverse ` A ) ) e. W )
41 1 2 3 4 efginvrel2 
 |-  ( ( M o. ( reverse ` A ) ) e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) .~ (/) )
42 40 41 syl 
 |-  ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) .~ (/) )
43 35 42 eqbrtrrd 
 |-  ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ A ) .~ (/) )