Step | Hyp | Ref
| Expression |
1 | | ralunb 3626 |
. . 3
 
    
 
       |
2 | | nfcv 2602 |
. . . . . . . . . . . . . . . . 17
   |
3 | | nfcsb1v 3390 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)  |
4 | | csbeq1a 3383 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
5 | 2, 3, 4 | cbvmpt 4507 |
. . . . . . . . . . . . . . . 16
             ![]_ ]_](_urbrack.gif)   |
6 | 5 | oveq2i 6325 |
. . . . . . . . . . . . . . 15
 g 
       g        ![]_ ]_](_urbrack.gif)    |
7 | | coe1fzgsumd.b |
. . . . . . . . . . . . . . . 16
     |
8 | | eqid 2461 |
. . . . . . . . . . . . . . . 16
       |
9 | | coe1fzgsumd.r |
. . . . . . . . . . . . . . . . . . . 20
   |
10 | | coe1fzgsumd.p |
. . . . . . . . . . . . . . . . . . . . 21
Poly1   |
11 | 10 | ply1ring 18889 |
. . . . . . . . . . . . . . . . . . . 20

  |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
13 | | ringcmn 17859 |
. . . . . . . . . . . . . . . . . . 19

CMnd |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 CMnd |
15 | 14 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . 17
 
 CMnd |
16 | 15 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
   
 
      CMnd |
17 | | simpll1 1053 |
. . . . . . . . . . . . . . . 16
   
 
        |
18 | | rspcsbela 3806 |
. . . . . . . . . . . . . . . . . . . 20
    
 ![]_ ]_](_urbrack.gif)
  |
19 | 18 | expcom 441 |
. . . . . . . . . . . . . . . . . . 19
 
   ![]_ ]_](_urbrack.gif)    |
20 | 19 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
    
  
 ![]_ ]_](_urbrack.gif)
   |
21 | 20 | adantr 471 |
. . . . . . . . . . . . . . . . 17
   
 
       
 ![]_ ]_](_urbrack.gif)
   |
22 | 21 | imp 435 |
. . . . . . . . . . . . . . . 16
    
 
 
  

   ![]_ ]_](_urbrack.gif)   |
23 | | vex 3059 |
. . . . . . . . . . . . . . . . 17
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
   
 
        |
25 | | simpll2 1054 |
. . . . . . . . . . . . . . . 16
   
 
     
  |
26 | | ssnid 4008 |
. . . . . . . . . . . . . . . . . 18
   |
27 | | rspcsbela 3806 |
. . . . . . . . . . . . . . . . . 18
           ![]_ ]_](_urbrack.gif)   |
28 | 26, 27 | mpan 681 |
. . . . . . . . . . . . . . . . 17
 
  
  ![]_ ]_](_urbrack.gif)
  |
29 | 28 | adantl 472 |
. . . . . . . . . . . . . . . 16
   
 
        ![]_ ]_](_urbrack.gif)   |
30 | | csbeq1 3377 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
31 | 7, 8, 16, 17, 22, 24, 25, 29, 30 | gsumunsn 17640 |
. . . . . . . . . . . . . . 15
   
 
       g        ![]_ ]_](_urbrack.gif)     g    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
32 | 6, 31 | syl5eq 2507 |
. . . . . . . . . . . . . 14
   
 
       g          g    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
33 | 2, 3, 4 | cbvmpt 4507 |
. . . . . . . . . . . . . . . . 17
     ![]_ ]_](_urbrack.gif)   |
34 | 33 | eqcomi 2470 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)     |
35 | 34 | oveq2i 6325 |
. . . . . . . . . . . . . . 15
 g    ![]_ ]_](_urbrack.gif)    g     |
36 | 35 | oveq1i 6324 |
. . . . . . . . . . . . . 14
  g    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    g           ![]_ ]_](_urbrack.gif)   |
37 | 32, 36 | syl6eq 2511 |
. . . . . . . . . . . . 13
   
 
       g          g           ![]_ ]_](_urbrack.gif)    |
38 | 37 | fveq2d 5891 |
. . . . . . . . . . . 12
   
 
      coe1 
g         coe1   g           ![]_ ]_](_urbrack.gif)     |
39 | 38 | fveq1d 5889 |
. . . . . . . . . . 11
   
 
       coe1  g             coe1   g 
         ![]_ ]_](_urbrack.gif)        |
40 | 9 | 3ad2ant3 1037 |
. . . . . . . . . . . . 13
 
   |
41 | 40 | ad2antrr 737 |
. . . . . . . . . . . 12
   
 
        |
42 | | simplr 767 |
. . . . . . . . . . . . 13
   
 
      
  |
43 | 7, 16, 17, 42 | gsummptcl 17647 |
. . . . . . . . . . . 12
   
 
       g      |
44 | | coe1fzgsumd.k |
. . . . . . . . . . . . . 14
   |
45 | 44 | 3ad2ant3 1037 |
. . . . . . . . . . . . 13
 
   |
46 | 45 | ad2antrr 737 |
. . . . . . . . . . . 12
   
 
        |
47 | | eqid 2461 |
. . . . . . . . . . . . 13
       |
48 | 10, 7, 8, 47 | coe1addfv 18906 |
. . . . . . . . . . . 12
    g      ![]_ ]_](_urbrack.gif)    coe1   g 
         ![]_ ]_](_urbrack.gif)        coe1  g              coe1   ![]_ ]_](_urbrack.gif)        |
49 | 41, 43, 29, 46, 48 | syl31anc 1279 |
. . . . . . . . . . 11
   
 
       coe1   g 
         ![]_ ]_](_urbrack.gif)        coe1  g              coe1   ![]_ ]_](_urbrack.gif)        |
50 | 39, 49 | eqtrd 2495 |
. . . . . . . . . 10
   
 
       coe1  g              coe1  g              coe1   ![]_ ]_](_urbrack.gif)        |
51 | | oveq1 6321 |
. . . . . . . . . 10
  coe1  g         g 
 coe1         coe1  g              coe1   ![]_ ]_](_urbrack.gif)        g   coe1             coe1   ![]_ ]_](_urbrack.gif)        |
52 | 50, 51 | sylan9eq 2515 |
. . . . . . . . 9
    
 
 
  

 coe1 
g         g   coe1       
 coe1 
g              g   coe1             coe1   ![]_ ]_](_urbrack.gif)        |
53 | | nfcv 2602 |
. . . . . . . . . . . . . 14
   coe1      |
54 | | nfcsb1v 3390 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  coe1      |
55 | | csbeq1a 3383 |
. . . . . . . . . . . . . 14
  coe1       ![]_ ]_](_urbrack.gif)  coe1       |
56 | 53, 54, 55 | cbvmpt 4507 |
. . . . . . . . . . . . 13
      coe1             ![]_ ]_](_urbrack.gif)  coe1       |
57 | 56 | oveq2i 6325 |
. . . . . . . . . . . 12
 g 
     coe1        g        ![]_ ]_](_urbrack.gif)  coe1        |
58 | | eqid 2461 |
. . . . . . . . . . . . 13
         |
59 | | ringcmn 17859 |
. . . . . . . . . . . . . . . 16

CMnd |
60 | 9, 59 | syl 17 |
. . . . . . . . . . . . . . 15
 CMnd |
61 | 60 | 3ad2ant3 1037 |
. . . . . . . . . . . . . 14
 
 CMnd |
62 | 61 | ad2antrr 737 |
. . . . . . . . . . . . 13
   
 
      CMnd |
63 | | csbfv12 5922 |
. . . . . . . . . . . . . . 15
  ![]_ ]_](_urbrack.gif)  coe1        ![]_ ]_](_urbrack.gif) coe1      ![]_ ]_](_urbrack.gif)   |
64 | | vex 3059 |
. . . . . . . . . . . . . . . . 17
 |
65 | | csbfv2g 5923 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif) coe1  coe1   ![]_ ]_](_urbrack.gif)    |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
  ![]_ ]_](_urbrack.gif) coe1  coe1   ![]_ ]_](_urbrack.gif)   |
67 | | csbconstg 3387 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
68 | 64, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
  ![]_ ]_](_urbrack.gif)  |
69 | 66, 68 | fveq12i 5892 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif) coe1      ![]_ ]_](_urbrack.gif)   coe1   ![]_ ]_](_urbrack.gif)      |
70 | 63, 69 | eqtri 2483 |
. . . . . . . . . . . . . 14
  ![]_ ]_](_urbrack.gif)  coe1      coe1   ![]_ ]_](_urbrack.gif)      |
71 | | eqid 2461 |
. . . . . . . . . . . . . . . . 17
coe1   ![]_ ]_](_urbrack.gif)  coe1   ![]_ ]_](_urbrack.gif)   |
72 | 71, 7, 10, 58 | coe1f 18852 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)
coe1   ![]_ ]_](_urbrack.gif)            |
73 | 22, 72 | syl 17 |
. . . . . . . . . . . . . . 15
    
 
 
  

 coe1   ![]_ ]_](_urbrack.gif)            |
74 | 45 | adantr 471 |
. . . . . . . . . . . . . . . 16
    
   |
75 | 74 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
    
 
 
  

   |
76 | 73, 75 | ffvelrnd 6045 |
. . . . . . . . . . . . . 14
    
 
 
  

  coe1   ![]_ ]_](_urbrack.gif)           |
77 | 70, 76 | syl5eqel 2543 |
. . . . . . . . . . . . 13
    
 
 
  

   ![]_ ]_](_urbrack.gif)  coe1           |
78 | | eqid 2461 |
. . . . . . . . . . . . . . . 16
coe1   ![]_ ]_](_urbrack.gif)  coe1   ![]_ ]_](_urbrack.gif)   |
79 | 78, 7, 10, 58 | coe1f 18852 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)
coe1   ![]_ ]_](_urbrack.gif)            |
80 | 29, 79 | syl 17 |
. . . . . . . . . . . . . 14
   
 
      coe1   ![]_ ]_](_urbrack.gif)            |
81 | 80, 46 | ffvelrnd 6045 |
. . . . . . . . . . . . 13
   
 
       coe1   ![]_ ]_](_urbrack.gif)           |
82 | | nfcv 2602 |
. . . . . . . . . . . . . 14
   |
83 | | nfcv 2602 |
. . . . . . . . . . . . . . . 16
 coe1 |
84 | | nfcsb1v 3390 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
85 | 83, 84 | nffv 5894 |
. . . . . . . . . . . . . . 15
  coe1   ![]_ ]_](_urbrack.gif)   |
86 | | nfcv 2602 |
. . . . . . . . . . . . . . 15
   |
87 | 85, 86 | nffv 5894 |
. . . . . . . . . . . . . 14
   coe1   ![]_ ]_](_urbrack.gif)      |
88 | | csbeq1a 3383 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
89 | 88 | fveq2d 5891 |
. . . . . . . . . . . . . . 15
 coe1  coe1   ![]_ ]_](_urbrack.gif)    |
90 | 89 | fveq1d 5889 |
. . . . . . . . . . . . . 14
  coe1      coe1   ![]_ ]_](_urbrack.gif)       |
91 | 82, 87, 90 | csbhypf 3393 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)  coe1      coe1   ![]_ ]_](_urbrack.gif)       |
92 | 58, 47, 62, 17, 77, 24, 25, 81, 91 | gsumunsn 17640 |
. . . . . . . . . . . 12
   
 
       g        ![]_ ]_](_urbrack.gif)  coe1         g    ![]_ ]_](_urbrack.gif)  coe1             coe1   ![]_ ]_](_urbrack.gif)        |
93 | 57, 92 | syl5eq 2507 |
. . . . . . . . . . 11
   
 
       g       coe1         g    ![]_ ]_](_urbrack.gif)  coe1             coe1   ![]_ ]_](_urbrack.gif)        |
94 | 53, 54, 55 | cbvmpt 4507 |
. . . . . . . . . . . . . 14
  coe1         ![]_ ]_](_urbrack.gif)  coe1       |
95 | 94 | eqcomi 2470 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)  coe1        coe1       |
96 | 95 | oveq2i 6325 |
. . . . . . . . . . . 12
 g    ![]_ ]_](_urbrack.gif)  coe1        g   coe1        |
97 | 96 | oveq1i 6324 |
. . . . . . . . . . 11
  g    ![]_ ]_](_urbrack.gif)  coe1             coe1   ![]_ ]_](_urbrack.gif)        g 
 coe1             coe1   ![]_ ]_](_urbrack.gif)       |
98 | 93, 97 | syl6req 2512 |
. . . . . . . . . 10
   
 
        g   coe1             coe1   ![]_ ]_](_urbrack.gif)       g       coe1         |
99 | 98 | adantr 471 |
. . . . . . . . 9
    
 
 
  

 coe1 
g         g   coe1       
  g   coe1             coe1   ![]_ ]_](_urbrack.gif)       g       coe1         |
100 | 52, 99 | eqtrd 2495 |
. . . . . . . 8
    
 
 
  

 coe1 
g         g   coe1       
 coe1 
g             g 
     coe1         |
101 | 100 | exp31 613 |
. . . . . . 7
    
  
     coe1  g         g   coe1        coe1  g             g 
     coe1           |
102 | 101 | com23 81 |
. . . . . 6
    
   coe1  g         g 
 coe1           
 coe1  g             g 
     coe1           |
103 | 102 | ex 440 |
. . . . 5
 
  
  coe1  g         g 
 coe1           
 coe1  g             g 
     coe1            |
104 | 103 | a2d 29 |
. . . 4
 
     coe1  g         g 
 coe1       
 
 
  
 coe1  g             g       coe1            |
105 | 104 | imp4b 599 |
. . 3
     
 coe1  g         g 
 coe1                  coe1  g             g       coe1          |
106 | 1, 105 | syl5bi 225 |
. 2
     
 coe1  g         g 
 coe1          
    
 coe1 
g             g 
     coe1          |
107 | 106 | ex 440 |
1
 
     coe1  g         g 
 coe1       
 
      coe1  g             g       coe1           |