Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . 5
         |
2 | | eqid 2193 |
. . . . 5
         |
3 | 1, 2 | mhm0 13030 |
. . . 4
  MndHom 
              |
4 | 3 | ad2antrr 488 |
. . 3
    MndHom 
Word 
               |
5 | | oveq2 5918 |
. . . . . 6

 g   g    |
6 | 5 | adantl 277 |
. . . . 5
    MndHom 
Word 
  g   g    |
7 | | mhmrcl1 13025 |
. . . . . . 7
  MndHom 
  |
8 | 7 | ad2antrr 488 |
. . . . . 6
    MndHom 
Word 

  |
9 | 1 | gsum0g 12969 |
. . . . . 6
  g 
      |
10 | 8, 9 | syl 14 |
. . . . 5
    MndHom 
Word 
  g 
      |
11 | 6, 10 | eqtrd 2226 |
. . . 4
    MndHom 
Word 
  g        |
12 | 11 | fveq2d 5550 |
. . 3
    MndHom 
Word 
     g             |
13 | | coeq2 4814 |
. . . . . . 7

      |
14 | | co02 5171 |
. . . . . . 7
   |
15 | 13, 14 | eqtrdi 2242 |
. . . . . 6

    |
16 | 15 | oveq2d 5926 |
. . . . 5

 g 
   g    |
17 | 16 | adantl 277 |
. . . 4
    MndHom 
Word 
  g     g    |
18 | | mhmrcl2 13026 |
. . . . . 6
  MndHom 
  |
19 | 18 | ad2antrr 488 |
. . . . 5
    MndHom 
Word 

  |
20 | 2 | gsum0g 12969 |
. . . . 5
  g 
      |
21 | 19, 20 | syl 14 |
. . . 4
    MndHom 
Word 
  g 
      |
22 | 17, 21 | eqtrd 2226 |
. . 3
    MndHom 
Word 
  g          |
23 | 4, 12, 22 | 3eqtr4d 2236 |
. 2
    MndHom 
Word 
     g    g      |
24 | 7 | ad2antrr 488 |
. . . . 5
    MndHom 
Word 

  |
25 | | gsumwmhm.b |
. . . . . . 7
     |
26 | | eqid 2193 |
. . . . . . 7
       |
27 | 25, 26 | mndcl 12994 |
. . . . . 6
 
          |
28 | 27 | 3expb 1206 |
. . . . 5
  
           |
29 | 24, 28 | sylan 283 |
. . . 4
     MndHom  Word 
             |
30 | | wrdf 10910 |
. . . . . . 7
 Word    ..^ ♯       |
31 | 30 | ad2antlr 489 |
. . . . . 6
    MndHom 
Word 
    ..^ ♯       |
32 | | wrdfin 10923 |
. . . . . . . . . . . 12
 Word   |
33 | 32 | adantl 277 |
. . . . . . . . . . 11
   MndHom  Word    |
34 | | hashnncl 10856 |
. . . . . . . . . . 11
  ♯ 
   |
35 | 33, 34 | syl 14 |
. . . . . . . . . 10
   MndHom  Word   ♯ 
   |
36 | 35 | biimpar 297 |
. . . . . . . . 9
    MndHom 
Word 
 ♯    |
37 | 36 | nnzd 9428 |
. . . . . . . 8
    MndHom 
Word 
 ♯    |
38 | | fzoval 10204 |
. . . . . . . 8
 ♯   ..^ ♯       ♯      |
39 | 37, 38 | syl 14 |
. . . . . . 7
    MndHom 
Word 
  ..^ ♯       ♯      |
40 | 39 | feq2d 5383 |
. . . . . 6
    MndHom 
Word 
     ..^ ♯    
      ♯         |
41 | 31, 40 | mpbid 147 |
. . . . 5
    MndHom 
Word 
       ♯        |
42 | 41 | ffvelcdmda 5685 |
. . . 4
     MndHom  Word 
     ♯           |
43 | | nnm1nn0 9271 |
. . . . . 6
 ♯   ♯     |
44 | 36, 43 | syl 14 |
. . . . 5
    MndHom 
Word 
  ♯     |
45 | | nn0uz 9617 |
. . . . 5
     |
46 | 44, 45 | eleqtrdi 2286 |
. . . 4
    MndHom 
Word 
  ♯         |
47 | | eqid 2193 |
. . . . . . 7
       |
48 | 25, 26, 47 | mhmlin 13029 |
. . . . . 6
   MndHom 
      
                      |
49 | 48 | 3expb 1206 |
. . . . 5
   MndHom  
 
                            |
50 | 49 | ad4ant14 514 |
. . . 4
     MndHom  Word 
                                |
51 | 41 | ffnd 5396 |
. . . . . 6
    MndHom 
Word 

    ♯      |
52 | | fvco2 5618 |
. . . . . 6
      ♯        ♯                     |
53 | 51, 52 | sylan 283 |
. . . . 5
     MndHom  Word 
     ♯                     |
54 | 53 | eqcomd 2199 |
. . . 4
     MndHom  Word 
     ♯                     |
55 | | simplr 528 |
. . . 4
    MndHom 
Word 

Word   |
56 | | coexg 5202 |
. . . . 5
   MndHom  Word  
   |
57 | 56 | adantr 276 |
. . . 4
    MndHom 
Word 
     |
58 | | plusgslid 12720 |
. . . . . . 7
 Slot      
  |
59 | 58 | slotex 12635 |
. . . . . 6
      |
60 | 7, 59 | syl 14 |
. . . . 5
  MndHom 
     |
61 | 60 | ad2antrr 488 |
. . . 4
    MndHom 
Word 
 
    |
62 | 58 | slotex 12635 |
. . . . . 6
      |
63 | 18, 62 | syl 14 |
. . . . 5
  MndHom 
     |
64 | 63 | ad2antrr 488 |
. . . 4
    MndHom 
Word 
 
    |
65 | 29, 42, 46, 50, 54, 55, 57, 61, 64 | seqhomog 10591 |
. . 3
    MndHom 
Word 
               ♯                  ♯      |
66 | 25, 26, 24, 46, 41 | gsumval2 12970 |
. . . 4
    MndHom 
Word 
  g             ♯      |
67 | 66 | fveq2d 5550 |
. . 3
    MndHom 
Word 
     g                 ♯       |
68 | | eqid 2193 |
. . . 4
         |
69 | 18 | ad2antrr 488 |
. . . 4
    MndHom 
Word 

  |
70 | 25, 68 | mhmf 13027 |
. . . . . 6
  MndHom 
          |
71 | 70 | ad2antrr 488 |
. . . . 5
    MndHom 
Word 
           |
72 | | fco 5411 |
. . . . 5
                ♯               ♯            |
73 | 71, 41, 72 | syl2anc 411 |
. . . 4
    MndHom 
Word 
         ♯            |
74 | 68, 47, 69, 46, 73 | gsumval2 12970 |
. . 3
    MndHom 
Word 
  g                 ♯      |
75 | 65, 67, 74 | 3eqtr4d 2236 |
. 2
    MndHom 
Word 
     g    g      |
76 | | fin0or 6933 |
. . . 4
 

   |
77 | | n0r 3460 |
. . . . 5
    |
78 | 77 | orim2i 762 |
. . . 4
  

    |
79 | 76, 78 | syl 14 |
. . 3
 
   |
80 | 33, 79 | syl 14 |
. 2
   MndHom  Word  
   |
81 | 23, 75, 80 | mpjaodan 799 |
1
   MndHom  Word      g    g      |