Step | Hyp | Ref
| Expression |
1 | | tsmssubm.s |
. . . . . 6
 SubMnd    |
2 | | tsmssubm.h |
. . . . . . 7

↾s   |
3 | 2 | submbas 16651 |
. . . . . 6
 SubMnd 
      |
4 | 1, 3 | syl 17 |
. . . . 5
       |
5 | 4 | eleq2d 2525 |
. . . 4
         |
6 | 5 | anbi1d 716 |
. . 3
                      g                   
 
  
 
    g          |
7 | | elin 3629 |
. . . . 5
   tsums     tsums     |
8 | | ancom 456 |
. . . . 5
   tsums  

 tsums     |
9 | 7, 8 | bitri 257 |
. . . 4
   tsums     tsums     |
10 | | eqid 2462 |
. . . . . . . . . 10
         |
11 | 10 | submss 16646 |
. . . . . . . . 9
 SubMnd 
      |
12 | 1, 11 | syl 17 |
. . . . . . . 8

      |
13 | 12 | sselda 3444 |
. . . . . . 7
 
       |
14 | | eqid 2462 |
. . . . . . . . 9
         |
15 | | eqid 2462 |
. . . . . . . . 9
       |
16 | | tsmssubm.1 |
. . . . . . . . 9
 CMnd |
17 | | tsmssubm.2 |
. . . . . . . . 9
   |
18 | | tsmssubm.a |
. . . . . . . . 9
   |
19 | | tsmssubm.f |
. . . . . . . . . 10
       |
20 | 19, 12 | fssd 5761 |
. . . . . . . . 9
           |
21 | 10, 14, 15, 16, 17, 18, 20 | eltsms 21196 |
. . . . . . . 8
   tsums 
    
                   g          |
22 | 21 | baibd 925 |
. . . . . . 7
 
    
  tsums  
      
 
  
 
    g         |
23 | 13, 22 | syldan 477 |
. . . . . 6
 
   tsums 
                   g         |
24 | | vex 3060 |
. . . . . . . . 9
 |
25 | 24 | inex1 4558 |
. . . . . . . 8
   |
26 | 25 | a1i 11 |
. . . . . . 7
        
    |
27 | 2, 14 | resstopn 20251 |
. . . . . . . . 9
     ↾t       |
28 | 27 | eleq2i 2532 |
. . . . . . . 8
     
↾t 
      |
29 | | fvex 5898 |
. . . . . . . . . 10
     |
30 | | elrest 15375 |
. . . . . . . . . 10
      SubMnd  
      ↾t 
           |
31 | 29, 1, 30 | sylancr 674 |
. . . . . . . . 9
       ↾t             |
32 | 31 | adantr 471 |
. . . . . . . 8
 
       ↾t  
          |
33 | 28, 32 | syl5bbr 267 |
. . . . . . 7
 
     
           |
34 | | eleq2 2529 |
. . . . . . . . 9
   

    |
35 | | elin 3629 |
. . . . . . . . . . 11
  

   |
36 | 35 | rbaib 922 |
. . . . . . . . . 10
   
   |
37 | 36 | adantl 472 |
. . . . . . . . 9
 
   
   |
38 | 34, 37 | sylan9bbr 712 |
. . . . . . . 8
           |
39 | | eleq2 2529 |
. . . . . . . . . . . . 13
     g     g         |
40 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
         |
41 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
         |
42 | 2 | submmnd 16650 |
. . . . . . . . . . . . . . . . . . . 20
 SubMnd 
  |
43 | 1, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
44 | 2 | subcmn 17526 |
. . . . . . . . . . . . . . . . . . 19
  CMnd  CMnd |
45 | 16, 43, 44 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
 CMnd |
46 | 45 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
        CMnd |
47 | | elfpw 7902 |
. . . . . . . . . . . . . . . . . . 19
   
    |
48 | 47 | simprbi 470 |
. . . . . . . . . . . . . . . . . 18
      |
49 | 48 | adantl 472 |
. . . . . . . . . . . . . . . . 17
          |
50 | 19 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
              |
51 | 47 | simplbi 466 |
. . . . . . . . . . . . . . . . . . . 20
      |
52 | 51 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
          |
53 | 50, 52 | fssresd 5773 |
. . . . . . . . . . . . . . . . . 18
                |
54 | 4 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
              |
55 | 54 | feq3d 5738 |
. . . . . . . . . . . . . . . . . 18
                            |
56 | 53, 55 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
                    |
57 | | fvex 5898 |
. . . . . . . . . . . . . . . . . . 19
     |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
              |
59 | 53, 49, 58 | fdmfifsupp 7919 |
. . . . . . . . . . . . . . . . 17
          finSupp       |
60 | 40, 41, 46, 49, 56, 59 | gsumcl 17598 |
. . . . . . . . . . . . . . . 16
         g          |
61 | 60, 54 | eleqtrrd 2543 |
. . . . . . . . . . . . . . 15
         g      |
62 | | elin 3629 |
. . . . . . . . . . . . . . . 16
  g        g     g 
     |
63 | 62 | rbaib 922 |
. . . . . . . . . . . . . . 15
  g      g       g       |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . 14
          g       g       |
65 | 1 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
        SubMnd    |
66 | 49, 65, 53, 2 | gsumsubm 16669 |
. . . . . . . . . . . . . . 15
         g     g      |
67 | 66 | eleq1d 2524 |
. . . . . . . . . . . . . 14
          g     g       |
68 | 64, 67 | bitr4d 264 |
. . . . . . . . . . . . 13
          g       g       |
69 | 39, 68 | sylan9bbr 712 |
. . . . . . . . . . . 12
   

 
 

 
  g     g       |
70 | 69 | an32s 818 |
. . . . . . . . . . 11
   


 
      g     g       |
71 | 70 | imbi2d 322 |
. . . . . . . . . 10
   


 
       g       g        |
72 | 71 | ralbidva 2836 |
. . . . . . . . 9
               g    
       g        |
73 | 72 | rexbidv 2913 |
. . . . . . . 8
                    g    
            g        |
74 | 38, 73 | imbi12d 326 |
. . . . . . 7
        
            g     

            g         |
75 | 26, 33, 74 | ralxfr2d 4630 |
. . . . . 6
 
  
      
 
  
 
    g     
                   g         |
76 | 23, 75 | bitr4d 264 |
. . . . 5
 
   tsums 
                   g         |
77 | 76 | pm5.32da 651 |
. . . 4
    tsums                       g          |
78 | 9, 77 | syl5bb 265 |
. . 3
    tsums  

                   g          |
79 | | eqid 2462 |
. . . 4
         |
80 | | resstps 20252 |
. . . . . 6
  SubMnd  
 ↾s    |
81 | 17, 1, 80 | syl2anc 671 |
. . . . 5
 
↾s    |
82 | 2, 81 | syl5eqel 2544 |
. . . 4
   |
83 | 4 | feq3d 5738 |
. . . . 5
                 |
84 | 19, 83 | mpbid 215 |
. . . 4
           |
85 | 40, 79, 15, 45, 82, 18, 84 | eltsms 21196 |
. . 3
   tsums 
    
                   g          |
86 | 6, 78, 85 | 3bitr4rd 294 |
. 2
   tsums 
  tsums 
    |
87 | 86 | eqrdv 2460 |
1
  tsums    tsums     |