Proof of Theorem gsumspl
Step | Hyp | Ref
| Expression |
1 | | gsumspl.eq |
. . . 4
  g   g    |
2 | 1 | oveq2d 6217 |
. . 3
   g  substr            g     g  substr            g     |
3 | 2 | oveq1d 6216 |
. 2
    g 
substr            g         g  substr              g 
substr            g         g  substr             |
4 | | gsumspl.s |
. . . . 5
 Word   |
5 | | gsumspl.f |
. . . . 5
       |
6 | | gsumspl.t |
. . . . 5
           |
7 | | gsumspl.x |
. . . . 5
 Word   |
8 | | splval 12512 |
. . . . 5
  Word 
   
        Word    splice
  
     substr     concat  concat  substr            |
9 | 4, 5, 6, 7, 8 | syl13anc 1221 |
. . . 4
  splice   
     substr     concat  concat  substr            |
10 | 9 | oveq2d 6217 |
. . 3
  g  splice   
    g    substr     concat 
concat  substr             |
11 | | gsumspl.m |
. . . 4
   |
12 | | swrdcl 12434 |
. . . . . 6
 Word  substr     Word   |
13 | 4, 12 | syl 16 |
. . . . 5
  substr     Word   |
14 | | ccatcl 12393 |
. . . . 5
   substr     Word
Word    substr     concat  Word   |
15 | 13, 7, 14 | syl2anc 661 |
. . . 4
   substr     concat
 Word   |
16 | | swrdcl 12434 |
. . . . 5
 Word  substr         Word   |
17 | 4, 16 | syl 16 |
. . . 4
  substr        
Word   |
18 | | gsumspl.b |
. . . . 5
     |
19 | | eqid 2454 |
. . . . 5
       |
20 | 18, 19 | gsumccat 15639 |
. . . 4
    substr     concat
 Word  substr         Word   g    substr     concat 
concat  substr             g   substr     concat         g  substr             |
21 | 11, 15, 17, 20 | syl3anc 1219 |
. . 3
  g    substr     concat 
concat  substr             g   substr     concat         g  substr             |
22 | 18, 19 | gsumccat 15639 |
. . . . 5
  
substr     Word
Word   g   substr     concat     g 
substr            g     |
23 | 11, 13, 7, 22 | syl3anc 1219 |
. . . 4
  g   substr     concat
    g  substr            g     |
24 | 23 | oveq1d 6216 |
. . 3
   g   substr     concat         g  substr              g  substr            g         g  substr             |
25 | 10, 21, 24 | 3eqtrd 2499 |
. 2
  g  splice   
      g  substr            g         g  substr             |
26 | | gsumspl.y |
. . . . 5
 Word   |
27 | | splval 12512 |
. . . . 5
  Word 
   
        Word    splice
  
     substr     concat  concat  substr            |
28 | 4, 5, 6, 26, 27 | syl13anc 1221 |
. . . 4
  splice   
     substr     concat  concat  substr            |
29 | 28 | oveq2d 6217 |
. . 3
  g  splice   
    g    substr     concat 
concat  substr             |
30 | | ccatcl 12393 |
. . . . 5
   substr     Word
Word    substr     concat  Word   |
31 | 13, 26, 30 | syl2anc 661 |
. . . 4
   substr     concat
 Word   |
32 | 18, 19 | gsumccat 15639 |
. . . 4
    substr     concat
 Word  substr         Word   g    substr     concat 
concat  substr             g   substr     concat         g  substr             |
33 | 11, 31, 17, 32 | syl3anc 1219 |
. . 3
  g    substr     concat 
concat  substr             g   substr     concat         g  substr             |
34 | 18, 19 | gsumccat 15639 |
. . . . 5
  
substr     Word
Word   g   substr     concat     g 
substr            g     |
35 | 11, 13, 26, 34 | syl3anc 1219 |
. . . 4
  g   substr     concat
    g  substr            g     |
36 | 35 | oveq1d 6216 |
. . 3
   g   substr     concat         g  substr              g  substr            g         g  substr             |
37 | 29, 33, 36 | 3eqtrd 2499 |
. 2
  g  splice   
      g  substr            g         g  substr             |
38 | 3, 25, 37 | 3eqtr4d 2505 |
1
  g  splice   
    g 
splice   
     |