Step | Hyp | Ref
| Expression |
1 | | cpmatsrngpmat.s |
. . . 4

ConstPolyMat   |
2 | | cpmatsrngpmat.p |
. . . 4
Poly1   |
3 | | cpmatsrngpmat.c |
. . . 4
 Mat   |
4 | | eqid 2471 |
. . . 4
         |
5 | 1, 2, 3, 4 | cpmatelimp 19813 |
. . 3
 
        

 coe1                 |
6 | 1, 2, 3, 4 | cpmatelimp 19813 |
. . . . . . . 8
 
        

 coe1                 |
7 | 6 | adantr 472 |
. . . . . . 7
   
     
    


  coe1                 |
8 | | ralcom 2937 |
. . . . . . . . . . . . . . . 16
 


 coe1             


 coe1               |
9 | | r19.26-2 2905 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  coe1              coe1             
 

 coe1                coe1                |
10 | | ralcom 2937 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  coe1              coe1             
    coe1              coe1                |
11 | 9, 10 | bitr3i 259 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 coe1                coe1             
    coe1              coe1                |
12 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 
   |
13 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      coe1              coe1               |
14 | 12, 13 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 
   
          
  coe1              coe1                |
15 | | simp-4r 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
     |
16 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
17 | | simplrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 
     |
18 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 
     |
19 | | simplrl 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
     
      
 
      |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 
         |
21 | 3, 16, 4, 17, 18, 20 | matecld 19528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
             |
22 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 
     |
23 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
     
      
 
      |
24 | 23 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 
         |
25 | 3, 16, 4, 18, 22, 24 | matecld 19528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
             |
26 | 15, 21, 25 | jca32 544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 
   
                     |
27 | 26 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
 
   
          
  coe1              coe1               

        
            |
28 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
           |
29 | 28 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 coe1      coe1        |
30 | 29 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
  coe1          coe1           |
31 | 30 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   coe1              coe1                |
32 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
           |
33 | 32 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 coe1      coe1        |
34 | 33 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
  coe1          coe1           |
35 | 34 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   coe1              coe1                |
36 | 31, 35 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    coe1              coe1                coe1              coe1                 |
37 | 36 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     coe1              coe1                 coe1              coe1                |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                 
        coe1              coe1                 coe1              coe1                 |
39 | 38 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
     
      
 


 
  coe1              coe1                coe1              coe1                   |
40 | 39 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
     
      
 

  
  coe1              coe1             
  coe1              coe1                   |
41 | 40 | imp31 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
 
   
        

  
  coe1              coe1                coe1              coe1                 |
42 | 41 | ralimdva 2805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
    
   coe1              coe1              
  coe1              coe1                 |
43 | 42 | impancom 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 
  

  coe1              coe1               
   coe1              coe1                 |
44 | 43 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
 
   
          
  coe1              coe1               
   coe1              coe1                |
45 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
46 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
47 | 2, 16, 45, 46 | cply1mul 18964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                         coe1              coe1             
  coe1                            |
48 | 27, 44, 47 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
 
   
          
  coe1              coe1               
  coe1                           |
49 | 48 | r19.21bi 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
          
  coe1              coe1               

 coe1                           |
50 | 49 | an32s 821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
          
  coe1              coe1                
 coe1                           |
51 | 50 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
 
   
          
  coe1              coe1                  coe1                              |
52 | 51 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
 
   
          
  coe1              coe1                 g   coe1                        g          |
53 | | ringmnd 17867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
54 | 53 | anim2i 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
     |
55 | 54 | ancomd 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
     |
56 | 45 | gsumz 16699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
  g              |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  g              |
58 | 57 | ad4antr 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
 
   
          
  coe1              coe1                 g              |
59 | 52, 58 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 
   
          
  coe1              coe1                 g   coe1                             |
60 | 59 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 
  

  coe1              coe1               
 g   coe1                              |
61 | 14, 60 | ralrimi 2800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 
  

  coe1              coe1                
g   coe1                             |
62 | | simp-4r 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
     |
63 | | nnnn0 10900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
64 | 63 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
     |
65 | 2 | ply1ring 18918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
66 | 65 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 
     |
67 | 16, 46 | ringcl 17872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
                               |
68 | 66, 21, 25, 67 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 
                         |
69 | 68 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     
      
 

                      |
70 | 69 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
   
                      |
71 | | simp-4l 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
     |
72 | 2, 16, 62, 64, 70, 71 | coe1fzgsumd 18973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
    coe1  g                         g   coe1                         |
73 | 72 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 
     coe1  g                           
 g   coe1                              |
74 | 73 | ralbidva 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
     
      
 
 
 coe1  g                           
  g   coe1                              |
75 | 74 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 
  

  coe1              coe1                  coe1  g                             
g   coe1                              |
76 | 61, 75 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 
  

  coe1              coe1                 coe1  g                              |
77 | 76 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     
      
 
 

  coe1              coe1              
 coe1  g                               |
78 | 11, 77 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . 21
   
     
      
 
  

 coe1                coe1              
 coe1  g                               |
79 | 78 | expd 443 |
. . . . . . . . . . . . . . . . . . . 20
   
     
      
 
 

 coe1              
  coe1               coe1  g                                |
80 | 79 | expr 626 |
. . . . . . . . . . . . . . . . . . 19
   
     
            coe1              

 coe1               coe1  g                                 |
81 | 80 | com23 80 |
. . . . . . . . . . . . . . . . . 18
   
     
        

 coe1             
 

 coe1               coe1  g                                 |
82 | 81 | imp31 439 |
. . . . . . . . . . . . . . . . 17
     
 
   
      

  coe1             
     coe1               coe1  g                               |
83 | 82 | ralimdva 2805 |
. . . . . . . . . . . . . . . 16
                
  
 coe1             
 


 coe1              
 coe1  g                               |
84 | 8, 83 | syl5bi 225 |
. . . . . . . . . . . . . . 15
                
  
 coe1             
 


 coe1              
 coe1  g                               |
85 | 84 | ex 441 |
. . . . . . . . . . . . . 14
   
     
        

 coe1              

  coe1             
  coe1  g                                |
86 | 85 | com23 80 |
. . . . . . . . . . . . 13
   
     
        


 coe1              
  coe1             
  coe1  g                                |
87 | 86 | impancom 447 |
. . . . . . . . . . . 12
   
     
      


 coe1             

 

 coe1              
 coe1  g                                |
88 | 87 | imp 436 |
. . . . . . . . . . 11
                  

 coe1                

 coe1              
 coe1  g                               |
89 | 88 | ralimdva 2805 |
. . . . . . . . . 10
   
     
      


 coe1             
 


 coe1              

 coe1  g                               |
90 | 89 | ex 441 |
. . . . . . . . 9
        
     
 


 coe1              

  coe1             

  coe1  g                                |
91 | 90 | expr 626 |
. . . . . . . 8
   
         
 


 coe1              

  coe1             

  coe1  g                                 |
92 | 91 | impd 438 |
. . . . . . 7
   
          


  coe1                   coe1             

  coe1  g                                |
93 | 7, 92 | syld 44 |
. . . . . 6
   
     
 


 coe1              

 coe1  g                                |
94 | 93 | com23 80 |
. . . . 5
   
      

  coe1              


 coe1  g                                |
95 | 94 | ex 441 |
. . . 4
 
           coe1              


 coe1  g                                 |
96 | 95 | impd 438 |
. . 3
 
      


  coe1                

 coe1  g                                |
97 | 5, 96 | syld 44 |
. 2
 
    

 coe1  g                                |
98 | 97 | imp32 440 |
1
    
  

  coe1  g                              |