Step | Hyp | Ref
| Expression |
1 | | tgptsmscls.2 |
. . . . . . . . . 10
   |
2 | 1 | adantr 471 |
. . . . . . . . 9
 

tsums     |
3 | | tgpgrp 21141 |
. . . . . . . . . . 11
   |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
 

tsums     |
5 | | eqid 2461 |
. . . . . . . . . . 11
         |
6 | 5 | 0subg 16890 |
. . . . . . . . . 10
       SubGrp    |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
 

tsums         SubGrp    |
8 | | tgptsmscls.j |
. . . . . . . . . 10
     |
9 | 8 | clssubg 21171 |
. . . . . . . . 9
        SubGrp                 SubGrp    |
10 | 2, 7, 9 | syl2anc 671 |
. . . . . . . 8
 

tsums                 SubGrp    |
11 | | tgptsmscls.b |
. . . . . . . . 9
     |
12 | | eqid 2461 |
. . . . . . . . 9
 ~QG                 ~QG                 |
13 | 11, 12 | eqger 16915 |
. . . . . . . 8
               SubGrp   ~QG                  |
14 | 10, 13 | syl 17 |
. . . . . . 7
 

tsums    ~QG                  |
15 | | tgptsmscls.1 |
. . . . . . . . . 10
 CMnd |
16 | | tgptps 21143 |
. . . . . . . . . . 11
   |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
   |
18 | | tgptsmscls.a |
. . . . . . . . . 10
   |
19 | | tgptsmscls.f |
. . . . . . . . . 10
       |
20 | 11, 15, 17, 18, 19 | tsmscl 21197 |
. . . . . . . . 9
  tsums    |
21 | 20 | sselda 3443 |
. . . . . . . 8
 

tsums     |
22 | | tgptsmscls.x |
. . . . . . . . . 10
  tsums    |
23 | 20, 22 | sseldd 3444 |
. . . . . . . . 9
   |
24 | 23 | adantr 471 |
. . . . . . . 8
 

tsums     |
25 | | eqid 2461 |
. . . . . . . . . 10
         |
26 | 15 | adantr 471 |
. . . . . . . . . 10
 

tsums   CMnd |
27 | 18 | adantr 471 |
. . . . . . . . . 10
 

tsums     |
28 | 19 | adantr 471 |
. . . . . . . . . 10
 

tsums         |
29 | 22 | adantr 471 |
. . . . . . . . . 10
 

tsums    tsums    |
30 | | simpr 467 |
. . . . . . . . . 10
 

tsums    tsums    |
31 | 11, 25, 26, 2, 27, 28, 28, 29, 30 | tsmssub 21211 |
. . . . . . . . 9
 

tsums            tsums             |
32 | 28 | ffvelrnda 6044 |
. . . . . . . . . . . . 13
    tsums          |
33 | 28 | feqmptd 5940 |
. . . . . . . . . . . . 13
 

tsums           |
34 | 27, 32, 32, 33, 33 | offval2 6574 |
. . . . . . . . . . . 12
 

tsums                                |
35 | 4 | adantr 471 |
. . . . . . . . . . . . . 14
    tsums      |
36 | 11, 5, 25 | grpsubid 16786 |
. . . . . . . . . . . . . 14
                             |
37 | 35, 32, 36 | syl2anc 671 |
. . . . . . . . . . . . 13
    tsums                          |
38 | 37 | mpteq2dva 4502 |
. . . . . . . . . . . 12
 

tsums                             |
39 | 34, 38 | eqtrd 2495 |
. . . . . . . . . . 11
 

tsums                    |
40 | 39 | oveq2d 6330 |
. . . . . . . . . 10
 

tsums    tsums            tsums          |
41 | 2, 16 | syl 17 |
. . . . . . . . . . 11
 

tsums     |
42 | 11, 5 | grpidcl 16742 |
. . . . . . . . . . . . . 14
       |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . 13
 

tsums         |
44 | 43 | adantr 471 |
. . . . . . . . . . . 12
    tsums          |
45 | | eqid 2461 |
. . . . . . . . . . . 12
             |
46 | 44, 45 | fmptd 6068 |
. . . . . . . . . . 11
 

tsums               |
47 | | fconstmpt 4896 |
. . . . . . . . . . . 12
               |
48 | | fvex 5897 |
. . . . . . . . . . . . . . 15
     |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
       |
50 | 18, 49 | fczfsuppd 7926 |
. . . . . . . . . . . . 13
         finSupp       |
51 | 50 | adantr 471 |
. . . . . . . . . . . 12
 

tsums           finSupp       |
52 | 47, 51 | syl5eqbrr 4450 |
. . . . . . . . . . 11
 

tsums         finSupp       |
53 | 11, 5, 26, 41, 27, 46, 52, 8 | tsmsgsum 21201 |
. . . . . . . . . 10
 

tsums    tsums                 g            |
54 | | cmnmnd 17493 |
. . . . . . . . . . . . . 14
 CMnd   |
55 | 26, 54 | syl 17 |
. . . . . . . . . . . . 13
 

tsums     |
56 | 5 | gsumz 16669 |
. . . . . . . . . . . . 13
 
  g              |
57 | 55, 27, 56 | syl2anc 671 |
. . . . . . . . . . . 12
 

tsums    g              |
58 | 57 | sneqd 3991 |
. . . . . . . . . . 11
 

tsums     g                 |
59 | 58 | fveq2d 5891 |
. . . . . . . . . 10
 

tsums            g                          |
60 | 40, 53, 59 | 3eqtrd 2499 |
. . . . . . . . 9
 

tsums    tsums                           |
61 | 31, 60 | eleqtrd 2541 |
. . . . . . . 8
 

tsums                           |
62 | | isabl 17482 |
. . . . . . . . . 10


CMnd  |
63 | 4, 26, 62 | sylanbrc 675 |
. . . . . . . . 9
 

tsums     |
64 | 11 | subgss 16866 |
. . . . . . . . . 10
               SubGrp               
  |
65 | 10, 64 | syl 17 |
. . . . . . . . 9
 

tsums                   |
66 | 11, 25, 12 | eqgabl 17523 |
. . . . . . . . 9
               
    ~QG                

                          |
67 | 63, 65, 66 | syl2anc 671 |
. . . . . . . 8
 

tsums      ~QG                

                          |
68 | 21, 24, 61, 67 | mpbir3and 1197 |
. . . . . . 7
 

tsums     ~QG                   |
69 | 14, 68 | ersym 7400 |
. . . . . 6
 

tsums     ~QG                   |
70 | 12 | releqg 16912 |
. . . . . . 7
 ~QG                 |
71 | | relelec 7429 |
. . . . . . 7
 
~QG                   ![] ]](rbrack.gif)  ~QG               
  ~QG                    |
72 | 70, 71 | ax-mp 5 |
. . . . . 6
   ![] ]](rbrack.gif) 
~QG               
  ~QG                   |
73 | 69, 72 | sylibr 217 |
. . . . 5
 

tsums     ![] ]](rbrack.gif)  ~QG                  |
74 | | eqid 2461 |
. . . . . . 7
                             |
75 | 11, 8, 5, 12, 74 | snclseqg 21178 |
. . . . . 6
     ![] ]](rbrack.gif)  ~QG                            |
76 | 2, 24, 75 | syl2anc 671 |
. . . . 5
 

tsums     ![] ]](rbrack.gif) 
~QG                            |
77 | 73, 76 | eleqtrd 2541 |
. . . 4
 

tsums               |
78 | 77 | ex 440 |
. . 3
   tsums 
             |
79 | 78 | ssrdv 3449 |
. 2
  tsums              |
80 | 11, 8, 15, 17, 18, 19, 22 | tsmscls 21200 |
. 2
            tsums    |
81 | 79, 80 | eqssd 3460 |
1
  tsums              |