Metamath Proof Explorer

Theorem efginvrel2

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 efginvrel2 
|- ( A e. W -> ( A ++ ( M o. ( reverse ` 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 id 
 |-  ( c = (/) -> c = (/) )
9 fveq2 
 |-  ( c = (/) -> ( reverse ` c ) = ( reverse ` (/) ) )
10 rev0 
 |-  ( reverse ` (/) ) = (/)
11 9 10 eqtrdi 
 |-  ( c = (/) -> ( reverse ` c ) = (/) )
12 11 coeq2d 
 |-  ( c = (/) -> ( M o. ( reverse ` c ) ) = ( M o. (/) ) )
13 co02 
 |-  ( M o. (/) ) = (/)
14 12 13 eqtrdi 
 |-  ( c = (/) -> ( M o. ( reverse ` c ) ) = (/) )
15 8 14 oveq12d 
 |-  ( c = (/) -> ( c ++ ( M o. ( reverse ` c ) ) ) = ( (/) ++ (/) ) )
16 15 breq1d 
 |-  ( c = (/) -> ( ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) <-> ( (/) ++ (/) ) .~ (/) ) )
17 16 imbi2d 
 |-  ( c = (/) -> ( ( A e. W -> ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) ) <-> ( A e. W -> ( (/) ++ (/) ) .~ (/) ) ) )
18 id 
 |-  ( c = a -> c = a )
19 fveq2 
 |-  ( c = a -> ( reverse ` c ) = ( reverse ` a ) )
20 19 coeq2d 
 |-  ( c = a -> ( M o. ( reverse ` c ) ) = ( M o. ( reverse ` a ) ) )
21 18 20 oveq12d 
 |-  ( c = a -> ( c ++ ( M o. ( reverse ` c ) ) ) = ( a ++ ( M o. ( reverse ` a ) ) ) )
22 21 breq1d 
 |-  ( c = a -> ( ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) <-> ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) ) )
23 22 imbi2d 
 |-  ( c = a -> ( ( A e. W -> ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) ) <-> ( A e. W -> ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) ) ) )
24 id 
 |-  ( c = ( a ++ <" b "> ) -> c = ( a ++ <" b "> ) )
25 fveq2 
 |-  ( c = ( a ++ <" b "> ) -> ( reverse ` c ) = ( reverse ` ( a ++ <" b "> ) ) )
26 25 coeq2d 
 |-  ( c = ( a ++ <" b "> ) -> ( M o. ( reverse ` c ) ) = ( M o. ( reverse ` ( a ++ <" b "> ) ) ) )
27 24 26 oveq12d 
 |-  ( c = ( a ++ <" b "> ) -> ( c ++ ( M o. ( reverse ` c ) ) ) = ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) )
28 27 breq1d 
 |-  ( c = ( a ++ <" b "> ) -> ( ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) <-> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) )
29 28 imbi2d 
 |-  ( c = ( a ++ <" b "> ) -> ( ( A e. W -> ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) ) <-> ( A e. W -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) ) )
30 id 
 |-  ( c = A -> c = A )
31 fveq2 
 |-  ( c = A -> ( reverse ` c ) = ( reverse ` A ) )
32 31 coeq2d 
 |-  ( c = A -> ( M o. ( reverse ` c ) ) = ( M o. ( reverse ` A ) ) )
33 30 32 oveq12d 
 |-  ( c = A -> ( c ++ ( M o. ( reverse ` c ) ) ) = ( A ++ ( M o. ( reverse ` A ) ) ) )
34 33 breq1d 
 |-  ( c = A -> ( ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) <-> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) ) )
35 34 imbi2d 
 |-  ( c = A -> ( ( A e. W -> ( c ++ ( M o. ( reverse ` c ) ) ) .~ (/) ) <-> ( A e. W -> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) ) ) )
36 ccatidid 
 |-  ( (/) ++ (/) ) = (/)
37 1 2 efger 
 |-  .~ Er W
38 37 a1i 
 |-  ( A e. W -> .~ Er W )
39 wrd0 
 |-  (/) e. Word ( I X. 2o )
40 1 efgrcl 
 |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
41 40 simprd 
 |-  ( A e. W -> W = Word ( I X. 2o ) )
42 39 41 eleqtrrid 
 |-  ( A e. W -> (/) e. W )
43 38 42 erref 
 |-  ( A e. W -> (/) .~ (/) )
44 36 43 eqbrtrid 
 |-  ( A e. W -> ( (/) ++ (/) ) .~ (/) )
45 37 a1i 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> .~ Er W )
46 simprl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> a e. Word ( I X. 2o ) )
47 revcl 
 |-  ( a e. Word ( I X. 2o ) -> ( reverse ` a ) e. Word ( I X. 2o ) )
48 47 ad2antrl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( reverse ` a ) e. Word ( I X. 2o ) )
49 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
50 wrdco 
 |-  ( ( ( reverse ` a ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) )
51 48 49 50 sylancl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) )
52 ccatcl 
 |-  ( ( a e. Word ( I X. 2o ) /\ ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) e. Word ( I X. 2o ) )
53 46 51 52 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) e. Word ( I X. 2o ) )
54 41 adantr 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> W = Word ( I X. 2o ) )
55 53 54 eleqtrrd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) e. W )
56 lencl 
 |-  ( a e. Word ( I X. 2o ) -> ( # ` a ) e. NN0 )
57 56 ad2antrl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. NN0 )
58 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
59 57 58 eleqtrdi 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. ( ZZ>= ` 0 ) )
60 ccatlen 
 |-  ( ( a e. Word ( I X. 2o ) /\ ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) ) -> ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) = ( ( # ` a ) + ( # ` ( M o. ( reverse ` a ) ) ) ) )
61 46 51 60 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) = ( ( # ` a ) + ( # ` ( M o. ( reverse ` a ) ) ) ) )
62 57 nn0zd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. ZZ )
63 62 uzidd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. ( ZZ>= ` ( # ` a ) ) )
64 lencl 
 |-  ( ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) -> ( # ` ( M o. ( reverse ` a ) ) ) e. NN0 )
65 51 64 syl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` ( M o. ( reverse ` a ) ) ) e. NN0 )
66 uzaddcl 
 |-  ( ( ( # ` a ) e. ( ZZ>= ` ( # ` a ) ) /\ ( # ` ( M o. ( reverse ` a ) ) ) e. NN0 ) -> ( ( # ` a ) + ( # ` ( M o. ( reverse ` a ) ) ) ) e. ( ZZ>= ` ( # ` a ) ) )
67 63 65 66 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` a ) + ( # ` ( M o. ( reverse ` a ) ) ) ) e. ( ZZ>= ` ( # ` a ) ) )
68 61 67 eqeltrd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) e. ( ZZ>= ` ( # ` a ) ) )
69 elfzuzb 
 |-  ( ( # ` a ) e. ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) <-> ( ( # ` a ) e. ( ZZ>= ` 0 ) /\ ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) e. ( ZZ>= ` ( # ` a ) ) ) )
70 59 68 69 sylanbrc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) )
71 simprr 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> b e. ( I X. 2o ) )
72 1 2 3 4 efgtval 
 |-  ( ( ( a ++ ( M o. ( reverse ` a ) ) ) e. W /\ ( # ` a ) e. ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) /\ b e. ( I X. 2o ) ) -> ( ( # ` a ) ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) b ) = ( ( a ++ ( M o. ( reverse ` a ) ) ) splice <. ( # ` a ) , ( # ` a ) , <" b ( M ` b ) "> >. ) )
73 55 70 71 72 syl3anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` a ) ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) b ) = ( ( a ++ ( M o. ( reverse ` a ) ) ) splice <. ( # ` a ) , ( # ` a ) , <" b ( M ` b ) "> >. ) )
74 39 a1i 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> (/) e. Word ( I X. 2o ) )
75 49 ffvelrni 
 |-  ( b e. ( I X. 2o ) -> ( M ` b ) e. ( I X. 2o ) )
76 75 ad2antll 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M ` b ) e. ( I X. 2o ) )
77 71 76 s2cld 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> <" b ( M ` b ) "> e. Word ( I X. 2o ) )
78 ccatrid 
 |-  ( a e. Word ( I X. 2o ) -> ( a ++ (/) ) = a )
79 78 ad2antrl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ (/) ) = a )
80 79 eqcomd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> a = ( a ++ (/) ) )
81 80 oveq1d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) = ( ( a ++ (/) ) ++ ( M o. ( reverse ` a ) ) ) )
82 eqidd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) = ( # ` a ) )
83 hash0 
 |-  ( # ` (/) ) = 0
84 83 oveq2i 
 |-  ( ( # ` a ) + ( # ` (/) ) ) = ( ( # ` a ) + 0 )
85 57 nn0cnd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) e. CC )
86 85 addid1d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` a ) + 0 ) = ( # ` a ) )
87 84 86 eqtr2id 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( # ` a ) = ( ( # ` a ) + ( # ` (/) ) ) )
88 46 74 51 77 81 82 87 splval2 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ ( M o. ( reverse ` a ) ) ) splice <. ( # ` a ) , ( # ` a ) , <" b ( M ` b ) "> >. ) = ( ( a ++ <" b ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) )
89 71 s1cld 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> <" b "> e. Word ( I X. 2o ) )
90 revccat 
 |-  ( ( a e. Word ( I X. 2o ) /\ <" b "> e. Word ( I X. 2o ) ) -> ( reverse ` ( a ++ <" b "> ) ) = ( ( reverse ` <" b "> ) ++ ( reverse ` a ) ) )
91 46 89 90 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( reverse ` ( a ++ <" b "> ) ) = ( ( reverse ` <" b "> ) ++ ( reverse ` a ) ) )
92 revs1 
 |-  ( reverse ` <" b "> ) = <" b ">
93 92 oveq1i 
 |-  ( ( reverse ` <" b "> ) ++ ( reverse ` a ) ) = ( <" b "> ++ ( reverse ` a ) )
94 91 93 eqtrdi 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( reverse ` ( a ++ <" b "> ) ) = ( <" b "> ++ ( reverse ` a ) ) )
95 94 coeq2d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M o. ( reverse ` ( a ++ <" b "> ) ) ) = ( M o. ( <" b "> ++ ( reverse ` a ) ) ) )
96 49 a1i 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> M : ( I X. 2o ) --> ( I X. 2o ) )
97 ccatco 
 |-  ( ( <" b "> e. Word ( I X. 2o ) /\ ( reverse ` a ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( <" b "> ++ ( reverse ` a ) ) ) = ( ( M o. <" b "> ) ++ ( M o. ( reverse ` a ) ) ) )
98 89 48 96 97 syl3anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M o. ( <" b "> ++ ( reverse ` a ) ) ) = ( ( M o. <" b "> ) ++ ( M o. ( reverse ` a ) ) ) )
99 s1co 
 |-  ( ( b e. ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. <" b "> ) = <" ( M ` b ) "> )
100 71 49 99 sylancl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M o. <" b "> ) = <" ( M ` b ) "> )
101 100 oveq1d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( M o. <" b "> ) ++ ( M o. ( reverse ` a ) ) ) = ( <" ( M ` b ) "> ++ ( M o. ( reverse ` a ) ) ) )
102 95 98 101 3eqtrd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( M o. ( reverse ` ( a ++ <" b "> ) ) ) = ( <" ( M ` b ) "> ++ ( M o. ( reverse ` a ) ) ) )
103 102 oveq2d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) = ( ( a ++ <" b "> ) ++ ( <" ( M ` b ) "> ++ ( M o. ( reverse ` a ) ) ) ) )
104 ccatcl 
 |-  ( ( a e. Word ( I X. 2o ) /\ <" b "> e. Word ( I X. 2o ) ) -> ( a ++ <" b "> ) e. Word ( I X. 2o ) )
105 46 89 104 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ <" b "> ) e. Word ( I X. 2o ) )
106 76 s1cld 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> <" ( M ` b ) "> e. Word ( I X. 2o ) )
107 ccatass 
 |-  ( ( ( a ++ <" b "> ) e. Word ( I X. 2o ) /\ <" ( M ` b ) "> e. Word ( I X. 2o ) /\ ( M o. ( reverse ` a ) ) e. Word ( I X. 2o ) ) -> ( ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) = ( ( a ++ <" b "> ) ++ ( <" ( M ` b ) "> ++ ( M o. ( reverse ` a ) ) ) ) )
108 105 106 51 107 syl3anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) = ( ( a ++ <" b "> ) ++ ( <" ( M ` b ) "> ++ ( M o. ( reverse ` a ) ) ) ) )
109 ccatass 
 |-  ( ( a e. Word ( I X. 2o ) /\ <" b "> e. Word ( I X. 2o ) /\ <" ( M ` b ) "> e. Word ( I X. 2o ) ) -> ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) = ( a ++ ( <" b "> ++ <" ( M ` b ) "> ) ) )
110 46 89 106 109 syl3anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) = ( a ++ ( <" b "> ++ <" ( M ` b ) "> ) ) )
111 df-s2 
 |-  <" b ( M ` b ) "> = ( <" b "> ++ <" ( M ` b ) "> )
112 111 oveq2i 
 |-  ( a ++ <" b ( M ` b ) "> ) = ( a ++ ( <" b "> ++ <" ( M ` b ) "> ) )
113 110 112 eqtr4di 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) = ( a ++ <" b ( M ` b ) "> ) )
114 113 oveq1d 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( ( a ++ <" b "> ) ++ <" ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) = ( ( a ++ <" b ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) )
115 103 108 114 3eqtr2rd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b ( M ` b ) "> ) ++ ( M o. ( reverse ` a ) ) ) = ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) )
116 73 88 115 3eqtrd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` a ) ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) b ) = ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) )
117 1 2 3 4 efgtf 
 |-  ( ( a ++ ( M o. ( reverse ` a ) ) ) e. W -> ( ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) = ( m e. ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) , u e. ( I X. 2o ) |-> ( ( a ++ ( M o. ( reverse ` a ) ) ) splice <. m , m , <" u ( M ` u ) "> >. ) ) /\ ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) : ( ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) X. ( I X. 2o ) ) --> W ) )
118 117 simprd 
 |-  ( ( a ++ ( M o. ( reverse ` a ) ) ) e. W -> ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) : ( ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) X. ( I X. 2o ) ) --> W )
119 55 118 syl 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) : ( ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) X. ( I X. 2o ) ) --> W )
120 119 ffnd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) Fn ( ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) X. ( I X. 2o ) ) )
121 fnovrn 
 |-  ( ( ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) Fn ( ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) X. ( I X. 2o ) ) /\ ( # ` a ) e. ( 0 ... ( # ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) /\ b e. ( I X. 2o ) ) -> ( ( # ` a ) ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) b ) e. ran ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) )
122 120 70 71 121 syl3anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( # ` a ) ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) b ) e. ran ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) )
123 116 122 eqeltrrd 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) e. ran ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) )
124 1 2 3 4 efgi2 
 |-  ( ( ( a ++ ( M o. ( reverse ` a ) ) ) e. W /\ ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) e. ran ( T ` ( a ++ ( M o. ( reverse ` a ) ) ) ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) .~ ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) )
125 55 123 124 syl2anc 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( a ++ ( M o. ( reverse ` a ) ) ) .~ ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) )
126 45 125 ersym 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ ( a ++ ( M o. ( reverse ` a ) ) ) )
127 45 ertr 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ ( a ++ ( M o. ( reverse ` a ) ) ) /\ ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) ) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) )
128 126 127 mpand 
 |-  ( ( A e. W /\ ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) ) -> ( ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) )
129 128 expcom 
 |-  ( ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) -> ( A e. W -> ( ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) ) )
130 129 a2d 
 |-  ( ( a e. Word ( I X. 2o ) /\ b e. ( I X. 2o ) ) -> ( ( A e. W -> ( a ++ ( M o. ( reverse ` a ) ) ) .~ (/) ) -> ( A e. W -> ( ( a ++ <" b "> ) ++ ( M o. ( reverse ` ( a ++ <" b "> ) ) ) ) .~ (/) ) ) )
131 17 23 29 35 44 130 wrdind 
 |-  ( A e. Word ( I X. 2o ) -> ( A e. W -> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) ) )
132 7 131 mpcom 
 |-  ( A e. W -> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) )