Step | Hyp | Ref
| Expression |
1 | | gsumzcl.g |
. . . . . . 7
   |
2 | | gsumzcl.a |
. . . . . . 7
   |
3 | | gsumzcl.0 |
. . . . . . . 8
     |
4 | 3 | gsumz 16699 |
. . . . . . 7
 
  g    |
5 | 1, 2, 4 | syl2anc 673 |
. . . . . 6
  g    |
6 | | gsumzf1o.h |
. . . . . . . . 9
       |
7 | | f1of1 5827 |
. . . . . . . . 9
    
      |
8 | 6, 7 | syl 17 |
. . . . . . . 8
       |
9 | | f1dmex 6782 |
. . . . . . . 8
     

  |
10 | 8, 2, 9 | syl2anc 673 |
. . . . . . 7
   |
11 | 3 | gsumz 16699 |
. . . . . . 7
 
  g    |
12 | 1, 10, 11 | syl2anc 673 |
. . . . . 6
  g    |
13 | 5, 12 | eqtr4d 2508 |
. . . . 5
  g    g     |
14 | 13 | adantr 472 |
. . . 4
 
 supp   g    g     |
15 | | gsumzcl.f |
. . . . . 6
       |
16 | | fvex 5889 |
. . . . . . . 8
     |
17 | 3, 16 | eqeltri 2545 |
. . . . . . 7
 |
18 | 17 | a1i 11 |
. . . . . 6
   |
19 | | ssid 3437 |
. . . . . . 7
 supp  supp  |
20 | 19 | a1i 11 |
. . . . . 6
  supp  supp   |
21 | 15, 2, 18, 20 | gsumcllem 17620 |
. . . . 5
 
 supp 

  |
22 | 21 | oveq2d 6324 |
. . . 4
 
 supp   g   g     |
23 | | f1of 5828 |
. . . . . . . . 9
    
      |
24 | 6, 23 | syl 17 |
. . . . . . . 8
       |
25 | 24 | adantr 472 |
. . . . . . 7
 
 supp        |
26 | 25 | ffvelrnda 6037 |
. . . . . 6
    supp  
      |
27 | 25 | feqmptd 5932 |
. . . . . 6
 
 supp 

       |
28 | | eqidd 2472 |
. . . . . 6
      |
29 | 26, 27, 21, 28 | fmptco 6072 |
. . . . 5
 
 supp       |
30 | 29 | oveq2d 6324 |
. . . 4
 
 supp   g     g     |
31 | 14, 22, 30 | 3eqtr4d 2515 |
. . 3
 
 supp   g   g      |
32 | 31 | ex 441 |
. 2
   supp
 g   g       |
33 | | coass 5361 |
. . . . . . . . . . 11
       
   |
34 | 6 | adantr 472 |
. . . . . . . . . . . . . 14
 
     supp           supp      supp
 
      |
35 | | f1ococnv2 5854 |
. . . . . . . . . . . . . 14
    
  
   |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
 
     supp           supp      supp
 
  
   |
37 | 36 | coeq1d 5001 |
. . . . . . . . . . . 12
 
     supp           supp      supp
 
 
        |
38 | | f1of1 5827 |
. . . . . . . . . . . . . . 15
          supp      supp
         supp      supp   |
39 | 38 | ad2antll 743 |
. . . . . . . . . . . . . 14
 
     supp           supp      supp
 
         supp      supp
  |
40 | | suppssdm 6946 |
. . . . . . . . . . . . . . . 16
 supp  |
41 | | fdm 5745 |
. . . . . . . . . . . . . . . . 17
       |
42 | 15, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
43 | 40, 42 | syl5sseq 3466 |
. . . . . . . . . . . . . . 15
  supp   |
44 | 43 | adantr 472 |
. . . . . . . . . . . . . 14
 
     supp           supp      supp
 
 supp
  |
45 | | f1ss 5797 |
. . . . . . . . . . . . . 14
           supp      supp  supp           supp       |
46 | 39, 44, 45 | syl2anc 673 |
. . . . . . . . . . . . 13
 
     supp           supp      supp
 
         supp       |
47 | | f1f 5792 |
. . . . . . . . . . . . 13
          supp    
         supp       |
48 | | fcoi2 5770 |
. . . . . . . . . . . . 13
          supp    
     |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . . 12
 
     supp           supp      supp
 
     |
50 | 37, 49 | eqtrd 2505 |
. . . . . . . . . . 11
 
     supp           supp      supp
 
 
     |
51 | 33, 50 | syl5reqr 2520 |
. . . . . . . . . 10
 
     supp           supp      supp
 

 
    |
52 | 51 | coeq2d 5002 |
. . . . . . . . 9
 
     supp           supp      supp
 
           |
53 | | coass 5361 |
. . . . . . . . 9
        
 
    |
54 | 52, 53 | syl6eqr 2523 |
. . . . . . . 8
 
     supp           supp      supp
 
           |
55 | 54 | seqeq3d 12259 |
. . . . . . 7
 
     supp           supp      supp
 
                           |
56 | 55 | fveq1d 5881 |
. . . . . 6
 
     supp           supp      supp
 
                supp                        supp     |
57 | | gsumzcl.b |
. . . . . . 7
     |
58 | | eqid 2471 |
. . . . . . 7
       |
59 | | gsumzcl.z |
. . . . . . 7
Cntz   |
60 | 1 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
  |
61 | 2 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
  |
62 | 15 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
      |
63 | | gsumzcl.c |
. . . . . . . 8
       |
64 | 63 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
      |
65 | | simprl 772 |
. . . . . . 7
 
     supp           supp      supp
 
    supp    |
66 | | f1ofo 5835 |
. . . . . . . . . 10
          supp      supp
         supp      supp   |
67 | | forn 5809 |
. . . . . . . . . 10
          supp      supp  supp
  |
68 | 66, 67 | syl 17 |
. . . . . . . . 9
          supp      supp
 supp   |
69 | 68 | ad2antll 743 |
. . . . . . . 8
 
     supp           supp      supp
 
 supp   |
70 | 19, 69 | syl5sseqr 3467 |
. . . . . . 7
 
     supp           supp      supp
 
 supp
  |
71 | | eqid 2471 |
. . . . . . 7
   supp    supp
 |
72 | 57, 3, 58, 59, 60, 61, 62, 64, 65, 46, 70, 71 | gsumval3 17619 |
. . . . . 6
 
     supp           supp      supp
 
 g                  supp     |
73 | 10 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
  |
74 | | fco 5751 |
. . . . . . . . 9
                   |
75 | 15, 24, 74 | syl2anc 673 |
. . . . . . . 8
         |
76 | 75 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
        |
77 | | rncoss 5101 |
. . . . . . . . 9

  |
78 | 59 | cntzidss 17069 |
. . . . . . . . 9
         

        |
79 | 63, 77, 78 | sylancl 675 |
. . . . . . . 8
           |
80 | 79 | adantr 472 |
. . . . . . 7
 
     supp           supp      supp
 
     
    |
81 | | f1ocnv 5840 |
. . . . . . . . . 10
    
       |
82 | | f1of1 5827 |
. . . . . . . . . 10
             |
83 | 6, 81, 82 | 3syl 18 |
. . . . . . . . 9
        |
84 | 83 | adantr 472 |
. . . . . . . 8
 
     supp           supp      supp
 
       |
85 | | f1co 5801 |
. . . . . . . 8
                supp       
          supp       |
86 | 84, 46, 85 | syl2anc 673 |
. . . . . . 7
 
     supp           supp      supp
 
 
          supp       |
87 | 19 | a1i 11 |
. . . . . . . . . . 11
 
     supp           supp      supp
 
 supp
 supp   |
88 | | fex 6155 |
. . . . . . . . . . . . . . 15
     
   |
89 | 15, 2, 88 | syl2anc 673 |
. . . . . . . . . . . . . 14
   |
90 | | suppimacnv 6944 |
. . . . . . . . . . . . . 14
    supp
         |
91 | 89, 17, 90 | sylancl 675 |
. . . . . . . . . . . . 13
  supp          |
92 | 91 | eqcomd 2477 |
. . . . . . . . . . . 12
         supp   |
93 | 92 | adantr 472 |
. . . . . . . . . . 11
 
     supp           supp      supp
 
        supp   |
94 | 87, 93, 69 | 3sstr4d 3461 |
. . . . . . . . . 10
 
     supp           supp      supp
 
      
  |
95 | | imass2 5210 |
. . . . . . . . . 10
                           |
96 | 94, 95 | syl 17 |
. . . . . . . . 9
 
     supp           supp      supp
 
                   |
97 | | cnvco 5025 |
. . . . . . . . . . 11
        |
98 | 97 | imaeq1i 5171 |
. . . . . . . . . 10
                    |
99 | | imaco 5347 |
. . . . . . . . . 10
  
                    |
100 | 98, 99 | eqtri 2493 |
. . . . . . . . 9
                      |
101 | | rnco2 5349 |
. . . . . . . . 9
 
       |
102 | 96, 100, 101 | 3sstr4g 3459 |
. . . . . . . 8
 
     supp           supp      supp
 
  
       
   |
103 | | f1oexrnex 6761 |
. . . . . . . . . . . . 13
     
   |
104 | 6, 2, 103 | syl2anc 673 |
. . . . . . . . . . . 12
   |
105 | | coexg 6763 |
. . . . . . . . . . . 12
 
     |
106 | 89, 104, 105 | syl2anc 673 |
. . . . . . . . . . 11
     |
107 | | suppimacnv 6944 |
. . . . . . . . . . 11
        supp
           |
108 | 106, 17, 107 | sylancl 675 |
. . . . . . . . . 10
    supp
           |
109 | 108 | sseq1d 3445 |
. . . . . . . . 9
     supp                   |
110 | 109 | adantr 472 |
. . . . . . . 8
 
     supp           supp      supp
 
    supp
  
  
       
    |
111 | 102, 110 | mpbird 240 |
. . . . . . 7
 
     supp           supp      supp
 
 
 supp
 
   |
112 | | eqid 2471 |
. . . . . . 7
        supp
        supp  |
113 | 57, 3, 58, 59, 60, 73, 76, 80, 65, 86, 111, 112 | gsumval3 17619 |
. . . . . 6
 
     supp           supp      supp
 
 g                         supp     |
114 | 56, 72, 113 | 3eqtr4d 2515 |
. . . . 5
 
     supp           supp      supp
 
 g   g 
    |
115 | 114 | expr 626 |
. . . 4
 
    supp             supp      supp
 g   g       |
116 | 115 | exlimdv 1787 |
. . 3
 
    supp    
         supp      supp  g   g       |
117 | 116 | expimpd 614 |
. 2
       supp            supp      supp 
 g   g 
     |
118 | | gsumzcl.w |
. . 3
 finSupp
 |
119 | | fsuppimp 7907 |
. . . 4
 finSupp   supp    |
120 | 119 | simprd 470 |
. . 3
 finSupp  supp
  |
121 | | fz1f1o 13853 |
. . 3
  supp
  supp      supp            supp      supp
    |
122 | 118, 120,
121 | 3syl 18 |
. 2
   supp
     supp            supp      supp
    |
123 | 32, 117, 122 | mpjaod 388 |
1
  g   g      |