Proof of Theorem chfacfpmmulgsum
Step | Hyp | Ref
| Expression |
1 | | eqid 2450 |
. . 3
         |
2 | | cayhamlem1.0 |
. . 3
     |
3 | | chfacfpmmulgsum.p |
. . 3
    |
4 | | crngring 17784 |
. . . . . . . 8

  |
5 | 4 | anim2i 572 |
. . . . . . 7
 
     |
6 | 5 | 3adant3 1027 |
. . . . . 6
 
 
   |
7 | | cayhamlem1.p |
. . . . . . 7
Poly1   |
8 | | cayhamlem1.y |
. . . . . . 7
 Mat   |
9 | 7, 8 | pmatring 19710 |
. . . . . 6
 

  |
10 | 6, 9 | syl 17 |
. . . . 5
 
   |
11 | | ringcmn 17804 |
. . . . 5

CMnd |
12 | 10, 11 | syl 17 |
. . . 4
 
 CMnd |
13 | 12 | adantr 467 |
. . 3
    
        CMnd |
14 | | nn0ex 10872 |
. . . 4
 |
15 | 14 | a1i 11 |
. . 3
    
       
  |
16 | | simpll 759 |
. . . . 5
   

          
   |
17 | | simplr 761 |
. . . . 5
   

          
         |
18 | | simpr 463 |
. . . . 5
   

            |
19 | 16, 17, 18 | 3jca 1187 |
. . . 4
   

             
      
   |
20 | | cayhamlem1.a |
. . . . 5
 Mat   |
21 | | cayhamlem1.b |
. . . . 5
     |
22 | | cayhamlem1.r |
. . . . 5
     |
23 | | cayhamlem1.s |
. . . . 5
     |
24 | | cayhamlem1.t |
. . . . 5

matToPolyMat   |
25 | | cayhamlem1.g |
. . . . 5
                     
                                                |
26 | | cayhamlem1.e |
. . . . 5
.g mulGrp    |
27 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 19878 |
. . . 4
    
      
       
           |
28 | 19, 27 | syl 17 |
. . 3
   

                
           |
29 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulfsupp 19880 |
. . 3
    
                      finSupp  |
30 | | nn0disj 11904 |
. . . 4
                 |
31 | 30 | a1i 11 |
. . 3
    
                          |
32 | | nnnn0 10873 |
. . . . . 6
   |
33 | | peano2nn0 10907 |
. . . . . 6

    |
34 | 32, 33 | syl 17 |
. . . . 5
     |
35 | | nn0split 11903 |
. . . . 5
  
                  |
36 | 34, 35 | syl 17 |
. . . 4
                   |
37 | 36 | ad2antrl 733 |
. . 3
    
       
                  |
38 | 1, 2, 3, 13, 15, 28, 29, 31, 37 | gsumsplit2 17555 |
. 2
    
         g 
 
              g         
            
g                
          |
39 | | simpll 759 |
. . . . . . . 8
   

                 
    |
40 | | simplr 761 |
. . . . . . . 8
   

                 
          |
41 | | nncn 10614 |
. . . . . . . . . . . . 13
   |
42 | | add1p1 10859 |
. . . . . . . . . . . . 13
         |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . 12
         |
44 | 43 | ad2antrl 733 |
. . . . . . . . . . 11
    
                |
45 | 44 | fveq2d 5867 |
. . . . . . . . . 10
    
                        |
46 | 45 | eleq2d 2513 |
. . . . . . . . 9
    
                          |
47 | 46 | biimpa 487 |
. . . . . . . 8
   

                 
        |
48 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmul0 19879 |
. . . . . . . 8
    
      
             
      |
49 | 39, 40, 47, 48 | syl3anc 1267 |
. . . . . . 7
   

                 
 
           |
50 | 49 | mpteq2dva 4488 |
. . . . . 6
    
                       
                 |
51 | 50 | oveq2d 6304 |
. . . . 5
    
         g                         g             |
52 | 4, 9 | sylan2 477 |
. . . . . . . . . 10
 

  |
53 | | ringmnd 17782 |
. . . . . . . . . 10

  |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
 

  |
55 | 54 | 3adant3 1027 |
. . . . . . . 8
 
   |
56 | | fvex 5873 |
. . . . . . . 8
         |
57 | 55, 56 | jctir 541 |
. . . . . . 7
 
 
           |
58 | 57 | adantr 467 |
. . . . . 6
    
        
           |
59 | 2 | gsumz 16614 |
. . . . . 6
            g            |
60 | 58, 59 | syl 17 |
. . . . 5
    
         g         
  |
61 | 51, 60 | eqtrd 2484 |
. . . 4
    
         g                         |
62 | 61 | oveq2d 6304 |
. . 3
    
          g              
        g                
          g              
         |
63 | 55 | adantr 467 |
. . . 4
    
          |
64 | | fzfid 12183 |
. . . . 5
    
                |
65 | | elfznn0 11884 |
. . . . . . . 8
         |
66 | 65, 19 | sylan2 477 |
. . . . . . 7
   

                   
      
   |
67 | 66, 27 | syl 17 |
. . . . . 6
   

                      
           |
68 | 67 | ralrimiva 2801 |
. . . . 5
    
                      
           |
69 | 1, 13, 64, 68 | gsummptcl 17592 |
. . . 4
    
         g         
                  |
70 | 1, 3, 2 | mndrid 16551 |
. . . 4
  
g              
              g         
           
 g              
         |
71 | 63, 69, 70 | syl2anc 666 |
. . 3
    
          g              
        g         
              |
72 | 62, 71 | eqtrd 2484 |
. 2
    
          g              
        g                
         g              
         |
73 | 32 | ad2antrl 733 |
. . . 4
    
          |
74 | 1, 3, 13, 73, 67 | gsummptfzsplit 17558 |
. . 3
    
         g         
              g       
            
g       
               |
75 | | elfznn0 11884 |
. . . . . . 7
       |
76 | 75, 28 | sylan2 477 |
. . . . . 6
   

                    
           |
77 | 1, 3, 13, 73, 76 | gsummptfzsplitl 17559 |
. . . . 5
    
         g       
              g       
            
g     
               |
78 | | 0nn0 10881 |
. . . . . . . 8
 |
79 | 78 | a1i 11 |
. . . . . . 7
    
          |
80 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 19878 |
. . . . . . . 8
    
      
       
           |
81 | 79, 80 | mpd3an3 1364 |
. . . . . . 7
    
                          |
82 | | oveq1 6295 |
. . . . . . . . 9
 
             |
83 | | fveq2 5863 |
. . . . . . . . 9
           |
84 | 82, 83 | oveq12d 6306 |
. . . . . . . 8
       
           
       |
85 | 1, 84 | gsumsn 17580 |
. . . . . . 7
 
      
           g     
                  
       |
86 | 63, 79, 81, 85 | syl3anc 1267 |
. . . . . 6
    
         g          
        
            |
87 | 86 | oveq2d 6304 |
. . . . 5
    
          g            
        g     
               g            
        
             |
88 | 77, 87 | eqtrd 2484 |
. . . 4
    
         g       
              g       
                  
        |
89 | | ovex 6316 |
. . . . . 6
   |
90 | 89 | a1i 11 |
. . . . 5
    
            |
91 | | 1nn0 10882 |
. . . . . . . 8
 |
92 | 91 | a1i 11 |
. . . . . . 7
    
          |
93 | 73, 92 | nn0addcld 10926 |
. . . . . 6
    
            |
94 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 19878 |
. . . . . 6
    
                  
             |
95 | 93, 94 | mpd3an3 1364 |
. . . . 5
    
                              |
96 | | oveq1 6295 |
. . . . . . 7
   
               |
97 | | fveq2 5863 |
. . . . . . 7
               |
98 | 96, 97 | oveq12d 6306 |
. . . . . 6
         
             
         |
99 | 1, 98 | gsumsn 17580 |
. . . . 5
            
             g       
                    
         |
100 | 63, 90, 95, 99 | syl3anc 1267 |
. . . 4
    
         g            
          
              |
101 | 88, 100 | oveq12d 6306 |
. . 3
    
          g            
        g       
                g            
        
                   
          |
102 | | fzfid 12183 |
. . . . . 6
    
              |
103 | | simpll 759 |
. . . . . . . 8
   

              
   |
104 | | simplr 761 |
. . . . . . . 8
   

              
         |
105 | | elfznn 11825 |
. . . . . . . . . 10
       |
106 | 105 | nnnn0d 10922 |
. . . . . . . . 9
       |
107 | 106 | adantl 468 |
. . . . . . . 8
   

                |
108 | 103, 104,
107, 27 | syl3anc 1267 |
. . . . . . 7
   

                    
           |
109 | 108 | ralrimiva 2801 |
. . . . . 6
    
                    
           |
110 | 1, 13, 102, 109 | gsummptcl 17592 |
. . . . 5
    
         g       
                  |
111 | 1, 3 | mndass 16539 |
. . . . 5
    g       
               
 
                      
                g            
        
                   
          g            
              
                         |
112 | 63, 110, 81, 95, 111 | syl13anc 1269 |
. . . 4
    
           g            
        
                   
          g            
              
                         |
113 | 25 | a1i 11 |
. . . . . . . . 9
   

                 
                                                  
                |
114 | 105 | nnne0d 10651 |
. . . . . . . . . . . . . 14
       |
115 | 114 | ad2antlr 732 |
. . . . . . . . . . . . 13
    
 
                |
116 | | neeq1 2685 |
. . . . . . . . . . . . . 14
     |
117 | 116 | adantl 468 |
. . . . . . . . . . . . 13
    
 
                  |
118 | 115, 117 | mpbird 236 |
. . . . . . . . . . . 12
    
 
                |
119 | | eqneqall 2633 |
. . . . . . . . . . . 12
               |
120 | 118, 119 | mpan9 472 |
. . . . . . . . . . 11
     
 
                           |
121 | | simplr 761 |
. . . . . . . . . . . . . . 15
     
 
              
  |
122 | | eqeq1 2454 |
. . . . . . . . . . . . . . . . 17
 
   |
123 | 122 | eqcoms 2458 |
. . . . . . . . . . . . . . . 16
 
   |
124 | 123 | adantl 468 |
. . . . . . . . . . . . . . 15
     
 
                   |
125 | 121, 124 | mpbird 236 |
. . . . . . . . . . . . . 14
     
 
                 |
126 | 125 | fveq2d 5867 |
. . . . . . . . . . . . 13
     
 
                         |
127 | 126 | fveq2d 5867 |
. . . . . . . . . . . 12
     
 
                                 |
128 | 127 | oveq2d 6304 |
. . . . . . . . . . 11
     
 
                                             |
129 | 120, 128 | oveq12d 6306 |
. . . . . . . . . 10
     
 
                   
                                      |
130 | | elfz2 11788 |
. . . . . . . . . . . . . . . . . 18
    
 
 
    |
131 | | zleltp1 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
132 | 131 | ancoms 455 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
133 | 132 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
     |
134 | 133 | biimpcd 228 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      |
135 | 134 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
136 | 135 | impcom 432 |
. . . . . . . . . . . . . . . . . . . 20
  
 
 
    |
137 | 136 | orcd 394 |
. . . . . . . . . . . . . . . . . . 19
  
 
 
        |
138 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
139 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
140 | 138, 139 | readdcld 9667 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
141 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
142 | 140, 141 | anim12ci 570 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
143 | 142 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
144 | | lttri2 9713 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
   
         |
146 | 145 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
  
 
 
            |
147 | 137, 146 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
  
 
 
    |
148 | 130, 147 | sylbi 199 |
. . . . . . . . . . . . . . . . 17
         |
149 | 148 | ad2antlr 732 |
. . . . . . . . . . . . . . . 16
    
 
                  |
150 | | neeq1 2685 |
. . . . . . . . . . . . . . . . 17
   
     |
151 | 150 | adantl 468 |
. . . . . . . . . . . . . . . 16
    
 
                
     |
152 | 149, 151 | mpbird 236 |
. . . . . . . . . . . . . . 15
    
 
                  |
153 | 152 | adantr 467 |
. . . . . . . . . . . . . 14
     
 
             
     |
154 | 153 | neneqd 2628 |
. . . . . . . . . . . . 13
     
 
             

    |
155 | 154 | pm2.21d 110 |
. . . . . . . . . . . 12
     
 
             
   
                                     |
156 | 155 | imp 431 |
. . . . . . . . . . 11
        
             
   
                                    |
157 | 105 | nnred 10621 |
. . . . . . . . . . . . . . . . . . 19
       |
158 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . 19
 
   |
159 | 157, 158 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . 18
     
   |
160 | 159 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   

              
   |
161 | 160 | imp 431 |
. . . . . . . . . . . . . . . 16
    
 
                |
162 | 73 | nn0red 10923 |
. . . . . . . . . . . . . . . . . 18
    
          |
163 | 162 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
    
 
                |
164 | | 1red 9655 |
. . . . . . . . . . . . . . . . 17
    
 
                |
165 | 163, 164 | readdcld 9667 |
. . . . . . . . . . . . . . . 16
    
 
                  |
166 | 130, 136 | sylbi 199 |
. . . . . . . . . . . . . . . . . 18
         |
167 | 166 | ad2antlr 732 |
. . . . . . . . . . . . . . . . 17
    
 
                  |
168 | | breq1 4404 |
. . . . . . . . . . . . . . . . . 18
 
 
     |
169 | 168 | adantl 468 |
. . . . . . . . . . . . . . . . 17
    
 
              
 
     |
170 | 167, 169 | mpbird 236 |
. . . . . . . . . . . . . . . 16
    
 
                  |
171 | 161, 165,
170 | ltnsymd 9781 |
. . . . . . . . . . . . . . 15
    
 
                  |
172 | 171 | pm2.21d 110 |
. . . . . . . . . . . . . 14
    
 
                                              |
173 | 172 | ad2antrr 731 |
. . . . . . . . . . . . 13
        
             
                                    |
174 | 173 | imp 431 |
. . . . . . . . . . . 12
       

              

     
                            |
175 | | simp-4r 776 |
. . . . . . . . . . . . . . . 16
       

              

        |
176 | 175 | oveq1d 6303 |
. . . . . . . . . . . . . . 15
       

              

            |
177 | 176 | fveq2d 5867 |
. . . . . . . . . . . . . 14
       

              

         
          |
178 | 177 | fveq2d 5867 |
. . . . . . . . . . . . 13
       

              

                            |
179 | 175 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
       

              

                |
180 | 179 | fveq2d 5867 |
. . . . . . . . . . . . . 14
       

              

                        |
181 | 180 | oveq2d 6304 |
. . . . . . . . . . . . 13
       

              

                                    |
182 | 178, 181 | oveq12d 6306 |
. . . . . . . . . . . 12
       

              

             
                                              |
183 | 174, 182 | ifeqda 3913 |
. . . . . . . . . . 11
        
             
                                                   
            |
184 | 156, 183 | ifeqda 3913 |
. . . . . . . . . 10
     
 
             
                                   
                                        |
185 | 129, 184 | ifeqda 3913 |
. . . . . . . . 9
    
 
               

    
                                             
                            
            |
186 | | ovex 6316 |
. . . . . . . . . 10
                           |
187 | 186 | a1i 11 |
. . . . . . . . 9
   

                                          |
188 | 113, 185,
107, 187 | fvmptd 5952 |
. . . . . . . 8
   

                                              |
189 | 188 | oveq2d 6304 |
. . . . . . 7
   

                    
           
                             |
190 | 189 | mpteq2dva 4488 |
. . . . . 6
    
                                     
                              |
191 | 190 | oveq2d 6304 |
. . . . 5
    
         g       
             g            
                               |
192 | 25 | a1i 11 |
. . . . . . . . 9
    
                
                                             
                |
193 | | nn0p1gt0 10896 |
. . . . . . . . . . . . . . 15

    |
194 | | 0red 9641 |
. . . . . . . . . . . . . . . . 17

  |
195 | | ltne 9727 |
. . . . . . . . . . . . . . . . 17
         |
196 | 194, 195 | sylan 474 |
. . . . . . . . . . . . . . . 16
         |
197 | | neeq1 2685 |
. . . . . . . . . . . . . . . 16
         |
198 | 196, 197 | syl5ibrcom 226 |
. . . . . . . . . . . . . . 15
           |
199 | 193, 198 | mpdan 673 |
. . . . . . . . . . . . . 14

      |
200 | 32, 199 | syl 17 |
. . . . . . . . . . . . 13
       |
201 | 200 | ad2antrl 733 |
. . . . . . . . . . . 12
    
          
   |
202 | 201 | imp 431 |
. . . . . . . . . . 11
   

              |
203 | | eqneqall 2633 |
. . . . . . . . . . 11
      
                     |
204 | 202, 203 | mpan9 472 |
. . . . . . . . . 10
    
 
                                     |
205 | | iftrue 3886 |
. . . . . . . . . . 11
    
                                                       |
206 | 205 | ad2antlr 732 |
. . . . . . . . . 10
    
 
                                                                     |
207 | 204, 206 | ifeqda 3913 |
. . . . . . . . 9
   

                                
                                                        |
208 | 73, 33 | syl 17 |
. . . . . . . . 9
    
            |
209 | | fvex 5873 |
. . . . . . . . . 10
         |
210 | 209 | a1i 11 |
. . . . . . . . 9
    
                  |
211 | 192, 207,
208, 210 | fvmptd 5952 |
. . . . . . . 8
    
                        |
212 | 211 | oveq2d 6304 |
. . . . . . 7
    
                           
                |
213 | 24, 20, 21, 7, 8 | mat2pmatbas 19743 |
. . . . . . . . . . . . 13
 
           |
214 | 4, 213 | syl3an2 1301 |
. . . . . . . . . . . 12
 
           |
215 | | eqid 2450 |
. . . . . . . . . . . . . 14
mulGrp  mulGrp   |
216 | 215, 1 | mgpbas 17722 |
. . . . . . . . . . . . 13
       mulGrp    |
217 | | eqid 2450 |
. . . . . . . . . . . . 13
   mulGrp      mulGrp    |
218 | 216, 217,
26 | mulg0 16756 |
. . . . . . . . . . . 12
        
         mulGrp     |
219 | 214, 218 | syl 17 |
. . . . . . . . . . 11
 
 
        mulGrp     |
220 | | eqid 2450 |
. . . . . . . . . . . 12
         |
221 | 215, 220 | ringidval 17730 |
. . . . . . . . . . 11
       mulGrp    |
222 | 219, 221 | syl6eqr 2502 |
. . . . . . . . . 10
 
 
           |
223 | 222 | adantr 467 |
. . . . . . . . 9
    
                    |
224 | 223 | oveq1d 6303 |
. . . . . . . 8
    
                                |
225 | 52 | 3adant3 1027 |
. . . . . . . . . 10
 
   |
226 | 225 | adantr 467 |
. . . . . . . . 9
    
          |
227 | 20, 21, 7, 8, 22, 23, 2, 24, 25 | chfacfisf 19871 |
. . . . . . . . . . 11
    
                  |
228 | 4, 227 | syl3anl2 1316 |
. . . . . . . . . 10
    
                  |
229 | 228, 79 | ffvelrnd 6021 |
. . . . . . . . 9
    
                  |
230 | 1, 22, 220 | ringlidm 17797 |
. . . . . . . . 9
               
           |
231 | 226, 229,
230 | syl2anc 666 |
. . . . . . . 8
    
                        |
232 | | iftrue 3886 |
. . . . . . . . . 10
  

    
                                             
                 
            |
233 | 232 | adantl 468 |
. . . . . . . . 9
   

                              
                                                               |
234 | | ovex 6316 |
. . . . . . . . . 10
                |
235 | 234 | a1i 11 |
. . . . . . . . 9
    
                         |
236 | 192, 233,
79, 235 | fvmptd 5952 |
. . . . . . . 8
    
           
                 |
237 | 224, 231,
236 | 3eqtrd 2488 |
. . . . . . 7
    
                                     |
238 | 212, 237 | oveq12d 6306 |
. . . . . 6
    
            
             
                    
        
                  |
239 | 1, 3 | cmncom 17439 |
. . . . . . 7
  CMnd       
        
   
                                 
                      
             
        |
240 | 13, 81, 95, 239 | syl3anc 1267 |
. . . . . 6
    
          
             
                      
             
        |
241 | | ringgrp 17778 |
. . . . . . . . 9

  |
242 | 10, 241 | syl 17 |
. . . . . . . 8
 
   |
243 | 242 | adantr 467 |
. . . . . . 7
    
          |
244 | 212, 95 | eqeltrrd 2529 |
. . . . . . 7
    
                                |
245 | 10 | adantr 467 |
. . . . . . . 8
    
          |
246 | 214 | adantr 467 |
. . . . . . . 8
    
                  |
247 | | simpl1 1010 |
. . . . . . . . 9
    
          |
248 | 4 | 3ad2ant2 1029 |
. . . . . . . . . 10
 
   |
249 | 248 | adantr 467 |
. . . . . . . . 9
    
          |
250 | | elmapi 7490 |
. . . . . . . . . . . 12
                 |
251 | 250 | adantl 468 |
. . . . . . . . . . 11
 
                 |
252 | 251 | adantl 468 |
. . . . . . . . . 10
    
                  |
253 | | 0elfz 11886 |
. . . . . . . . . . . 12

      |
254 | 32, 253 | syl 17 |
. . . . . . . . . . 11
       |
255 | 254 | ad2antrl 733 |
. . . . . . . . . 10
    
              |
256 | 252, 255 | ffvelrnd 6021 |
. . . . . . . . 9
    
              |
257 | 24, 20, 21, 7, 8 | mat2pmatbas 19743 |
. . . . . . . . 9
 
                   |
258 | 247, 249,
256, 257 | syl3anc 1267 |
. . . . . . . 8
    
                      |
259 | 1, 22 | ringcl 17787 |
. . . . . . . 8
         
            
                    |
260 | 245, 246,
258, 259 | syl3anc 1267 |
. . . . . . 7
    
                            |
261 | 1, 2, 23, 3 | grpsubadd0sub 16734 |
. . . . . . 7
          
            
                  
         
                                 
        
                  |
262 | 243, 244,
260, 261 | syl3anc 1267 |
. . . . . 6
    
            
                                 
                                |
263 | 238, 240,
262 | 3eqtr4d 2494 |
. . . . 5
    
          
             
                      
                          |
264 | 191, 263 | oveq12d 6306 |
. . . 4
    
          g            
              
                         g       
                    
                                                  |
265 | 112, 264 | eqtrd 2484 |
. . 3
    
           g            
        
                   
          g            
                                 
                                |
266 | 74, 101, 265 | 3eqtrd 2488 |
. 2
    
         g         
              g       
                    
                                                  |
267 | 38, 72, 266 | 3eqtrd 2488 |
1
    
         g 
 
              g       
                    
                                                  |