Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
Word     |
2 | | fviss 5938 |
. . . 4
Word    Word    |
3 | 1, 2 | eqsstri 3448 |
. . 3
Word    |
4 | 3 | sseli 3414 |
. 2
 Word     |
5 | | id 22 |
. . . . . 6

  |
6 | | fveq2 5879 |
. . . . . . . . 9

reverse  reverse    |
7 | | rev0 12923 |
. . . . . . . . 9
reverse   |
8 | 6, 7 | syl6eq 2521 |
. . . . . . . 8

reverse    |
9 | 8 | coeq2d 5002 |
. . . . . . 7

 reverse       |
10 | | co02 5356 |
. . . . . . 7
   |
11 | 9, 10 | syl6eq 2521 |
. . . . . 6

 reverse     |
12 | 5, 11 | oveq12d 6326 |
. . . . 5

 ++  reverse     ++    |
13 | 12 | breq1d 4405 |
. . . 4

  ++  reverse   
 ++     |
14 | 13 | imbi2d 323 |
. . 3

   ++  reverse     
 ++      |
15 | | id 22 |
. . . . . 6
   |
16 | | fveq2 5879 |
. . . . . . 7
 reverse  reverse    |
17 | 16 | coeq2d 5002 |
. . . . . 6
 
reverse    reverse     |
18 | 15, 17 | oveq12d 6326 |
. . . . 5
  ++  reverse     ++  reverse      |
19 | 18 | breq1d 4405 |
. . . 4
   ++  reverse     ++  reverse       |
20 | 19 | imbi2d 323 |
. . 3
    ++  reverse     
 ++ 
reverse        |
21 | | id 22 |
. . . . . 6
  ++       ++        |
22 | | fveq2 5879 |
. . . . . . 7
  ++      reverse  reverse  ++         |
23 | 22 | coeq2d 5002 |
. . . . . 6
  ++       reverse    reverse  ++          |
24 | 21, 23 | oveq12d 6326 |
. . . . 5
  ++       ++  reverse      ++      ++ 
reverse  ++           |
25 | 24 | breq1d 4405 |
. . . 4
  ++        ++  reverse      ++      ++  reverse  ++            |
26 | 25 | imbi2d 323 |
. . 3
  ++       
 ++ 
reverse    

  ++      ++  reverse  ++             |
27 | | id 22 |
. . . . . 6
   |
28 | | fveq2 5879 |
. . . . . . 7
 reverse  reverse    |
29 | 28 | coeq2d 5002 |
. . . . . 6
 
reverse    reverse     |
30 | 27, 29 | oveq12d 6326 |
. . . . 5
  ++  reverse     ++  reverse      |
31 | 30 | breq1d 4405 |
. . . 4
   ++  reverse     ++  reverse       |
32 | 31 | imbi2d 323 |
. . 3
    ++  reverse     
 ++ 
reverse        |
33 | | wrd0 12742 |
. . . . 5
Word    |
34 | | ccatlid 12781 |
. . . . 5
 Word    ++    |
35 | 33, 34 | ax-mp 5 |
. . . 4
 ++ 
 |
36 | | efgval.r |
. . . . . . 7
~FG    |
37 | 1, 36 | efger 17446 |
. . . . . 6
 |
38 | 37 | a1i 11 |
. . . . 5
   |
39 | 1 | efgrcl 17443 |
. . . . . . 7
 
Word      |
40 | 39 | simprd 470 |
. . . . . 6
 Word     |
41 | 33, 40 | syl5eleqr 2556 |
. . . . 5
   |
42 | 38, 41 | erref 7401 |
. . . 4
   |
43 | 35, 42 | syl5eqbr 4429 |
. . 3
  ++    |
44 | 37 | a1i 11 |
. . . . . . 7
   Word         |
45 | | simprl 772 |
. . . . . . . . . 10
   Word       Word     |
46 | | revcl 12920 |
. . . . . . . . . . . 12
 Word  
reverse  Word
    |
47 | 46 | ad2antrl 742 |
. . . . . . . . . . 11
   Word       reverse  Word     |
48 | | efgval2.m |
. . . . . . . . . . . 12
 
       |
49 | 48 | efgmf 17441 |
. . . . . . . . . . 11
         |
50 | | wrdco 12987 |
. . . . . . . . . . 11
  reverse  Word            
reverse   Word     |
51 | 47, 49, 50 | sylancl 675 |
. . . . . . . . . 10
   Word       
reverse   Word     |
52 | | ccatcl 12771 |
. . . . . . . . . 10
  Word   
reverse   Word     ++  reverse    Word     |
53 | 45, 51, 52 | syl2anc 673 |
. . . . . . . . 9
   Word        ++  reverse    Word     |
54 | 40 | adantr 472 |
. . . . . . . . 9
   Word       Word     |
55 | 53, 54 | eleqtrrd 2552 |
. . . . . . . 8
   Word        ++  reverse      |
56 | | lencl 12737 |
. . . . . . . . . . . . . 14
 Word  
      |
57 | 56 | ad2antrl 742 |
. . . . . . . . . . . . 13
   Word             |
58 | | nn0uz 11217 |
. . . . . . . . . . . . 13
     |
59 | 57, 58 | syl6eleq 2559 |
. . . . . . . . . . . 12
   Word                 |
60 | | ccatlen 12772 |
. . . . . . . . . . . . . 14
  Word   
reverse   Word        ++  reverse              reverse       |
61 | 45, 51, 60 | syl2anc 673 |
. . . . . . . . . . . . 13
   Word           ++  reverse              reverse       |
62 | 57 | nn0zd 11061 |
. . . . . . . . . . . . . . 15
   Word             |
63 | | uzid 11197 |
. . . . . . . . . . . . . . 15
    
              |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
   Word                     |
65 | | lencl 12737 |
. . . . . . . . . . . . . . 15
  reverse   Word      
reverse      |
66 | 51, 65 | syl 17 |
. . . . . . . . . . . . . 14
   Word           reverse      |
67 | | uzaddcl 11238 |
. . . . . . . . . . . . . 14
                  reverse              reverse               |
68 | 64, 66, 67 | syl2anc 673 |
. . . . . . . . . . . . 13
   Word               
reverse               |
69 | 61, 68 | eqeltrd 2549 |
. . . . . . . . . . . 12
   Word           ++  reverse               |
70 | | elfzuzb 11820 |
. . . . . . . . . . . 12
            ++  reverse                   ++  reverse                |
71 | 59, 69, 70 | sylanbrc 677 |
. . . . . . . . . . 11
   Word                  ++  reverse        |
72 | | simprr 774 |
. . . . . . . . . . 11
   Word           |
73 | | efgval2.t |
. . . . . . . . . . . 12
              splice                  |
74 | 1, 36, 48, 73 | efgtval 17451 |
. . . . . . . . . . 11
   ++  reverse               ++  reverse                   ++  reverse         ++  reverse    splice                         |
75 | 55, 71, 72, 74 | syl3anc 1292 |
. . . . . . . . . 10
   Word                 ++  reverse         ++  reverse    splice                         |
76 | 33 | a1i 11 |
. . . . . . . . . . 11
   Word       Word     |
77 | 49 | ffvelrni 6036 |
. . . . . . . . . . . . 13
  
        |
78 | 72, 77 | syl 17 |
. . . . . . . . . . . 12
   Word               |
79 | 72, 78 | s2cld 13025 |
. . . . . . . . . . 11
   Word                Word     |
80 | | ccatrid 12782 |
. . . . . . . . . . . . . 14
 Word  
 ++ 
  |
81 | 80 | ad2antrl 742 |
. . . . . . . . . . . . 13
   Word        ++    |
82 | 81 | eqcomd 2477 |
. . . . . . . . . . . 12
   Word        ++    |
83 | 82 | oveq1d 6323 |
. . . . . . . . . . 11
   Word        ++  reverse      ++  ++  reverse      |
84 | | eqidd 2472 |
. . . . . . . . . . 11
   Word                 |
85 | | hash0 12586 |
. . . . . . . . . . . . 13
     |
86 | 85 | oveq2i 6319 |
. . . . . . . . . . . 12
                 |
87 | 57 | nn0cnd 10951 |
. . . . . . . . . . . . 13
   Word             |
88 | 87 | addid1d 9851 |
. . . . . . . . . . . 12
   Word                   |
89 | 86, 88 | syl5req 2518 |
. . . . . . . . . . 11
   Word                       |
90 | 45, 76, 51, 79, 83, 84, 89 | splval2 12918 |
. . . . . . . . . 10
   Word         ++  reverse    splice                         ++           ++  reverse      |
91 | 72 | s1cld 12795 |
. . . . . . . . . . . . . . . 16
   Word           Word
    |
92 | | revccat 12925 |
. . . . . . . . . . . . . . . 16
  Word       Word    reverse  ++        reverse      ++ reverse     |
93 | 45, 91, 92 | syl2anc 673 |
. . . . . . . . . . . . . . 15
   Word       reverse  ++        reverse      ++ reverse     |
94 | | revs1 12924 |
. . . . . . . . . . . . . . . 16
reverse           |
95 | 94 | oveq1i 6318 |
. . . . . . . . . . . . . . 15
 reverse      ++ reverse        ++ reverse    |
96 | 93, 95 | syl6eq 2521 |
. . . . . . . . . . . . . 14
   Word       reverse  ++            ++ reverse     |
97 | 96 | coeq2d 5002 |
. . . . . . . . . . . . 13
   Word       
reverse  ++              ++ reverse      |
98 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
   Word                 |
99 | | ccatco 12991 |
. . . . . . . . . . . . . 14
      Word   reverse  Word
           
     ++ reverse           ++  reverse      |
100 | 91, 47, 98, 99 | syl3anc 1292 |
. . . . . . . . . . . . 13
   Word       
     ++ reverse           ++  reverse      |
101 | | s1co 12989 |
. . . . . . . . . . . . . . 15
             
               |
102 | 72, 49, 101 | sylancl 675 |
. . . . . . . . . . . . . 14
   Word       
               |
103 | 102 | oveq1d 6323 |
. . . . . . . . . . . . 13
   Word              ++ 
reverse             ++  reverse      |
104 | 97, 100, 103 | 3eqtrd 2509 |
. . . . . . . . . . . 12
   Word       
reverse  ++                 ++  reverse      |
105 | 104 | oveq2d 6324 |
. . . . . . . . . . 11
   Word         ++      ++  reverse  ++           ++      ++          ++  reverse       |
106 | | ccatcl 12771 |
. . . . . . . . . . . . 13
  Word       Word     ++      Word     |
107 | 45, 91, 106 | syl2anc 673 |
. . . . . . . . . . . 12
   Word        ++      Word     |
108 | 78 | s1cld 12795 |
. . . . . . . . . . . 12
   Word               Word
    |
109 | | ccatass 12783 |
. . . . . . . . . . . 12
   ++      Word           Word
  
reverse   Word   
   ++      ++          ++  reverse      ++      ++          ++  reverse       |
110 | 107, 108,
51, 109 | syl3anc 1292 |
. . . . . . . . . . 11
   Word          ++      ++          ++  reverse      ++      ++          ++  reverse       |
111 | | ccatass 12783 |
. . . . . . . . . . . . . 14
  Word       Word           Word
     ++      ++         
 ++      ++             |
112 | 45, 91, 108, 111 | syl3anc 1292 |
. . . . . . . . . . . . 13
   Word         ++      ++           ++      ++             |
113 | | df-s2 13003 |
. . . . . . . . . . . . . 14
              ++           |
114 | 113 | oveq2i 6319 |
. . . . . . . . . . . . 13
 ++            ++      ++            |
115 | 112, 114 | syl6eqr 2523 |
. . . . . . . . . . . 12
   Word         ++      ++           ++             |
116 | 115 | oveq1d 6323 |
. . . . . . . . . . 11
   Word          ++      ++          ++  reverse      ++           ++  reverse      |
117 | 105, 110,
116 | 3eqtr2rd 2512 |
. . . . . . . . . 10
   Word         ++           ++ 
reverse      ++      ++  reverse  ++           |
118 | 75, 90, 117 | 3eqtrd 2509 |
. . . . . . . . 9
   Word                 ++  reverse         ++      ++  reverse  ++           |
119 | 1, 36, 48, 73 | efgtf 17450 |
. . . . . . . . . . . 12
  ++  reverse         ++
 reverse             ++  reverse           ++  reverse    splice                    ++  reverse               ++  reverse              |
120 | 119 | simprd 470 |
. . . . . . . . . . 11
  ++  reverse        ++  reverse               ++  reverse             |
121 | | ffn 5739 |
. . . . . . . . . . 11
     ++  reverse               ++  reverse          
    ++  reverse             ++  reverse           |
122 | 55, 120, 121 | 3syl 18 |
. . . . . . . . . 10
   Word           ++ 
reverse             ++  reverse           |
123 | | fnovrn 6463 |
. . . . . . . . . 10
      ++  reverse             ++  reverse                    ++  reverse     
             ++
 reverse           ++ 
reverse       |
124 | 122, 71, 72, 123 | syl3anc 1292 |
. . . . . . . . 9
   Word                 ++  reverse           ++  reverse       |
125 | 118, 124 | eqeltrrd 2550 |
. . . . . . . 8
   Word         ++      ++  reverse  ++             ++ 
reverse       |
126 | 1, 36, 48, 73 | efgi2 17453 |
. . . . . . . 8
   ++  reverse      ++      ++  reverse  ++             ++ 
reverse       ++  reverse      ++      ++  reverse  ++           |
127 | 55, 125, 126 | syl2anc 673 |
. . . . . . 7
   Word        ++  reverse      ++      ++  reverse  ++           |
128 | 44, 127 | ersym 7393 |
. . . . . 6
   Word         ++      ++  reverse  ++          ++  reverse      |
129 | 44 | ertr 7396 |
. . . . . 6
   Word           ++      ++  reverse  ++          ++  reverse     ++  reverse    
  ++      ++  reverse  ++            |
130 | 128, 129 | mpand 689 |
. . . . 5
   Word         ++  reverse      ++      ++ 
reverse  ++            |
131 | 130 | expcom 442 |
. . . 4
  Word  
      ++  reverse      ++      ++ 
reverse  ++             |
132 | 131 | a2d 28 |
. . 3
  Word  
    
 ++ 
reverse     
  ++      ++  reverse  ++             |
133 | 14, 20, 26, 32, 43, 132 | wrdind 12887 |
. 2
 Word  
  ++  reverse       |
134 | 4, 133 | mpcom 36 |
1
  ++  reverse      |