Step | Hyp | Ref
| Expression |
1 | | eqidd 2454 |
. . . . 5
   

     
 g       g      decompPMat             decompPMat               g       g      decompPMat             decompPMat              |
2 | | oveq1 6302 |
. . . . . . . . . . 11
    decompPMat       decompPMat      |
3 | | oveq2 6303 |
. . . . . . . . . . 11
    decompPMat         decompPMat        |
4 | 2, 3 | oveqan12d 6314 |
. . . . . . . . . 10
 
     decompPMat             decompPMat           decompPMat             decompPMat         |
5 | 4 | mpteq2dv 4493 |
. . . . . . . . 9
 
      decompPMat             decompPMat             decompPMat             decompPMat          |
6 | 5 | oveq2d 6311 |
. . . . . . . 8
 
  g      decompPMat             decompPMat          g      decompPMat             decompPMat           |
7 | 6 | mpteq2dv 4493 |
. . . . . . 7
 
       g      decompPMat             decompPMat                g      decompPMat             decompPMat            |
8 | 7 | oveq2d 6311 |
. . . . . 6
 
  g       g      decompPMat             decompPMat            g       g      decompPMat             decompPMat             |
9 | 8 | adantl 468 |
. . . . 5
       
 

   g       g      decompPMat             decompPMat            g       g      decompPMat             decompPMat             |
10 | | simprl 765 |
. . . . 5
   

      |
11 | | simprr 767 |
. . . . 5
   

      |
12 | | ovex 6323 |
. . . . . 6
 g       g      decompPMat             decompPMat            |
13 | 12 | a1i 11 |
. . . . 5
   

     g       g      decompPMat             decompPMat             |
14 | 1, 9, 10, 11, 13 | ovmpt2d 6429 |
. . . 4
   

         g       g      decompPMat             decompPMat               g       g      decompPMat             decompPMat             |
15 | | decpmatmul.c |
. . . . . . . . . . . . . . . . . . . 20
 Mat   |
16 | | decpmatmul.b |
. . . . . . . . . . . . . . . . . . . 20
     |
17 | 15, 16 | matrcl 19449 |
. . . . . . . . . . . . . . . . . . 19
 
   |
18 | 17 | simpld 461 |
. . . . . . . . . . . . . . . . . 18
   |
19 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
20 | 19 | anim2i 573 |
. . . . . . . . . . . . . . . 16
  
 

   |
21 | 20 | ancomd 453 |
. . . . . . . . . . . . . . 15
  
 
    |
22 | 21 | 3adant3 1029 |
. . . . . . . . . . . . . 14
  

 
   |
23 | | decpmatmul.a |
. . . . . . . . . . . . . . 15
 Mat   |
24 | | eqid 2453 |
. . . . . . . . . . . . . . 15
 maMul       maMul       |
25 | 23, 24 | matmulr 19475 |
. . . . . . . . . . . . . 14
 
  maMul
  
        |
26 | 22, 25 | syl 17 |
. . . . . . . . . . . . 13
  

  maMul   
        |
27 | 26 | adantr 467 |
. . . . . . . . . . . 12
   

     maMul
  
        |
28 | 27 | adantr 467 |
. . . . . . . . . . 11
       
 
      maMul            |
29 | 28 | eqcomd 2459 |
. . . . . . . . . 10
       
 
          maMul   
    |
30 | 29 | oveqd 6312 |
. . . . . . . . 9
       
 
      
decompPMat         decompPMat
      decompPMat    maMul        decompPMat 
     |
31 | | eqid 2453 |
. . . . . . . . . 10
         |
32 | | eqid 2453 |
. . . . . . . . . 10
         |
33 | | simp1 1009 |
. . . . . . . . . . . 12
  

   |
34 | 33 | adantr 467 |
. . . . . . . . . . 11
   

   
  |
35 | 34 | adantr 467 |
. . . . . . . . . 10
       
 
       |
36 | 22 | simpld 461 |
. . . . . . . . . . . 12
  

   |
37 | 36 | adantr 467 |
. . . . . . . . . . 11
   

   
  |
38 | 37 | adantr 467 |
. . . . . . . . . 10
       
 
       |
39 | | simpl2l 1062 |
. . . . . . . . . . . . . 14
   

   
  |
40 | 39 | adantr 467 |
. . . . . . . . . . . . 13
       
 
       |
41 | | elfznn0 11894 |
. . . . . . . . . . . . . 14
       |
42 | 41 | adantl 468 |
. . . . . . . . . . . . 13
       
 
       |
43 | 35, 40, 42 | 3jca 1189 |
. . . . . . . . . . . 12
       
 
     
   |
44 | | decpmatmul.p |
. . . . . . . . . . . . 13
Poly1   |
45 | | eqid 2453 |
. . . . . . . . . . . . 13
         |
46 | 44, 15, 16, 23, 45 | decpmatcl 19803 |
. . . . . . . . . . . 12
 
  decompPMat        |
47 | 43, 46 | syl 17 |
. . . . . . . . . . 11
       
 
      decompPMat        |
48 | 23, 31, 45 | matbas2i 19459 |
. . . . . . . . . . 11
  decompPMat       decompPMat
     
     |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
       
 
      decompPMat      
     |
50 | | simpl2r 1063 |
. . . . . . . . . . . . . 14
   

   
  |
51 | 50 | adantr 467 |
. . . . . . . . . . . . 13
       
 
       |
52 | | fznn0sub 11838 |
. . . . . . . . . . . . . 14
     
   |
53 | 52 | adantl 468 |
. . . . . . . . . . . . 13
       
 
     
   |
54 | 35, 51, 53 | 3jca 1189 |
. . . . . . . . . . . 12
       
 
     

    |
55 | 44, 15, 16, 23, 45 | decpmatcl 19803 |
. . . . . . . . . . . 12
 

   decompPMat          |
56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
       
 
      decompPMat          |
57 | 23, 31, 45 | matbas2i 19459 |
. . . . . . . . . . 11
  decompPMat         decompPMat
             |
58 | 56, 57 | syl 17 |
. . . . . . . . . 10
       
 
      decompPMat        
     |
59 | 24, 31, 32, 35, 38, 38, 38, 49, 58 | mamuval 19423 |
. . . . . . . . 9
       
 
      
decompPMat    maMul        decompPMat 
    
 g      decompPMat             decompPMat            |
60 | 30, 59 | eqtrd 2487 |
. . . . . . . 8
       
 
      
decompPMat         decompPMat
       g      decompPMat             decompPMat            |
61 | 60 | mpteq2dva 4492 |
. . . . . . 7
   

           decompPMat         decompPMat              g      decompPMat             decompPMat             |
62 | 61 | oveq2d 6311 |
. . . . . 6
   

     g        decompPMat         decompPMat        g       
 g      decompPMat             decompPMat              |
63 | | eqid 2453 |
. . . . . . 7
         |
64 | | ovex 6323 |
. . . . . . . 8
     |
65 | 64 | a1i 11 |
. . . . . . 7
   

          |
66 | | ringcmn 17823 |
. . . . . . . . . . . . 13

CMnd |
67 | 33, 66 | syl 17 |
. . . . . . . . . . . 12
  

 CMnd |
68 | 67 | adantr 467 |
. . . . . . . . . . 11
   

   
CMnd |
69 | 68 | adantr 467 |
. . . . . . . . . 10
       
 
     CMnd |
70 | 69 | 3ad2ant1 1030 |
. . . . . . . . 9
    


   
    

CMnd |
71 | 38 | 3ad2ant1 1030 |
. . . . . . . . 9
    


   
    

  |
72 | 35 | 3ad2ant1 1030 |
. . . . . . . . . . . 12
    


   
    

  |
73 | 72 | adantr 467 |
. . . . . . . . . . 11
      

   
    

   |
74 | | simpl2 1013 |
. . . . . . . . . . . 12
      

   
    

   |
75 | | simpr 463 |
. . . . . . . . . . . 12
      

   
    

   |
76 | 43 | 3ad2ant1 1030 |
. . . . . . . . . . . . . 14
    


   
    


   |
77 | 76 | adantr 467 |
. . . . . . . . . . . . 13
      

   
    

 
   |
78 | 77, 46 | syl 17 |
. . . . . . . . . . . 12
      

   
    

  decompPMat        |
79 | 23, 31, 45, 74, 75, 78 | matecld 19463 |
. . . . . . . . . . 11
      

   
    

    decompPMat          |
80 | | simpl3 1014 |
. . . . . . . . . . . 12
      

   
    

   |
81 | 56 | 3ad2ant1 1030 |
. . . . . . . . . . . . 13
    


   
    

 decompPMat          |
82 | 81 | adantr 467 |
. . . . . . . . . . . 12
      

   
    

  decompPMat          |
83 | 23, 31, 45, 75, 80, 82 | matecld 19463 |
. . . . . . . . . . 11
      

   
    

    decompPMat            |
84 | 31, 32 | ringcl 17806 |
. . . . . . . . . . 11
     decompPMat           decompPMat 
             decompPMat             decompPMat             |
85 | 73, 79, 83, 84 | syl3anc 1269 |
. . . . . . . . . 10
      

   
    

     decompPMat             decompPMat             |
86 | 85 | ralrimiva 2804 |
. . . . . . . . 9
    


   
    


    decompPMat             decompPMat             |
87 | 31, 70, 71, 86 | gsummptcl 17611 |
. . . . . . . 8
    


   
    

 g      decompPMat             decompPMat               |
88 | 23, 31, 45, 38, 35, 87 | matbas2d 19460 |
. . . . . . 7
       
 
        g      decompPMat             decompPMat                |
89 | | eqid 2453 |
. . . . . . . 8
        g      decompPMat             decompPMat                   g      decompPMat             decompPMat            |
90 | | fzfid 12193 |
. . . . . . . 8
   

          |
91 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
   |
92 | 91, 91 | jca 535 |
. . . . . . . . . . . . . 14
 
     |
93 | 17, 92 | syl 17 |
. . . . . . . . . . . . 13
 
   |
94 | 93 | adantr 467 |
. . . . . . . . . . . 12
 
     |
95 | 94 | 3ad2ant2 1031 |
. . . . . . . . . . 11
  

 
   |
96 | 95 | adantr 467 |
. . . . . . . . . 10
   

        |
97 | 96 | adantr 467 |
. . . . . . . . 9
       
 
     
   |
98 | | mpt2exga 6874 |
. . . . . . . . 9
 
  
 g      decompPMat             decompPMat            |
99 | 97, 98 | syl 17 |
. . . . . . . 8
       
 
        g      decompPMat             decompPMat            |
100 | | fvex 5880 |
. . . . . . . . 9
     |
101 | 100 | a1i 11 |
. . . . . . . 8
   

          |
102 | 89, 90, 99, 101 | fsuppmptdm 7899 |
. . . . . . 7
   

          
 g      decompPMat             decompPMat           finSupp       |
103 | 23, 45, 63, 37, 65, 34, 88, 102 | matgsum 19474 |
. . . . . 6
   

     g       
 g      decompPMat             decompPMat               g       g      decompPMat             decompPMat              |
104 | 62, 103 | eqtrd 2487 |
. . . . 5
   

     g        decompPMat         decompPMat        
 g       g      decompPMat             decompPMat              |
105 | 104 | oveqd 6312 |
. . . 4
   

       g        decompPMat         decompPMat            
 g       g      decompPMat             decompPMat                |
106 | | simpl2 1013 |
. . . . . 6
   

    
   |
107 | | simpl3 1014 |
. . . . . 6
   

   
  |
108 | 44, 15, 16 | decpmatmullem 19807 |
. . . . . 6
    


             decompPMat     g   g        coe1                coe1                  |
109 | 37, 34, 106, 10, 11, 107, 108 | syl213anc 1288 |
. . . . 5
   

               decompPMat     g   g        coe1                coe1                  |
110 | | simpll1 1048 |
. . . . . . 7
       
 

     
  |
111 | | simplrl 771 |
. . . . . . . . 9
       
 

        |
112 | | simprl 765 |
. . . . . . . . 9
       
 

        |
113 | 16 | eleq2i 2523 |
. . . . . . . . . . . . . 14

      |
114 | 113 | biimpi 198 |
. . . . . . . . . . . . 13
       |
115 | 114 | adantr 467 |
. . . . . . . . . . . 12
 
       |
116 | 115 | 3ad2ant2 1031 |
. . . . . . . . . . 11
  

       |
117 | 116 | adantr 467 |
. . . . . . . . . 10
   

   
      |
118 | 117 | adantr 467 |
. . . . . . . . 9
       
 

     
      |
119 | | eqid 2453 |
. . . . . . . . . 10
         |
120 | 15, 119 | matecl 19462 |
. . . . . . . . 9
 
               |
121 | 111, 112,
118, 120 | syl3anc 1269 |
. . . . . . . 8
       
 

                |
122 | 41 | ad2antll 736 |
. . . . . . . 8
       
 

        |
123 | | eqid 2453 |
. . . . . . . . 9
coe1      coe1       |
124 | 123, 119,
44, 31 | coe1fvalcl 18817 |
. . . . . . . 8
            coe1               |
125 | 121, 122,
124 | syl2anc 667 |
. . . . . . 7
       
 

       coe1               |
126 | | simplrr 772 |
. . . . . . . . 9
       
 

        |
127 | 50 | adantr 467 |
. . . . . . . . 9
       
 

     
  |
128 | 15, 119, 16, 112, 126, 127 | matecld 19463 |
. . . . . . . 8
       
 

                |
129 | 52 | ad2antll 736 |
. . . . . . . 8
       
 

          |
130 | | eqid 2453 |
. . . . . . . . 9
coe1      coe1       |
131 | 130, 119,
44, 31 | coe1fvalcl 18817 |
. . . . . . . 8
          
   coe1        
        |
132 | 128, 129,
131 | syl2anc 667 |
. . . . . . 7
       
 

       coe1        
        |
133 | 31, 32 | ringcl 17806 |
. . . . . . 7
   coe1              coe1        
      
  coe1                coe1        
         |
134 | 110, 125,
132, 133 | syl3anc 1269 |
. . . . . 6
       
 

        coe1                coe1                  |
135 | 31, 68, 37, 90, 134 | gsumcom3fi 19437 |
. . . . 5
   

     g   g        coe1                coe1                 g       g    coe1                coe1                  |
136 | 43 | adantr 467 |
. . . . . . . . . . . 12
    


   
     

   |
137 | 10 | adantr 467 |
. . . . . . . . . . . . 13
       
 
       |
138 | 137 | anim1i 572 |
. . . . . . . . . . . 12
    


   
     

   |
139 | 44, 15, 16 | decpmate 19802 |
. . . . . . . . . . . 12
  
 
     decompPMat     coe1           |
140 | 136, 138,
139 | syl2anc 667 |
. . . . . . . . . . 11
    


   
     
  
decompPMat     coe1           |
141 | 54 | adantr 467 |
. . . . . . . . . . . 12
    


   
     

     |
142 | | simplrr 772 |
. . . . . . . . . . . . . 14
       
 
       |
143 | 142 | anim1i 572 |
. . . . . . . . . . . . 13
    


   
     

   |
144 | 143 | ancomd 453 |
. . . . . . . . . . . 12
    


   
     

   |
145 | 44, 15, 16 | decpmate 19802 |
. . . . . . . . . . . 12
   
  
     decompPMat       coe1        
    |
146 | 141, 144,
145 | syl2anc 667 |
. . . . . . . . . . 11
    


   
     
  
decompPMat       coe1        
    |
147 | 140, 146 | oveq12d 6313 |
. . . . . . . . . 10
    


   
     
    decompPMat             decompPMat         coe1                coe1              |
148 | 147 | eqcomd 2459 |
. . . . . . . . 9
    


   
     
  coe1                coe1        
       decompPMat             decompPMat         |
149 | 148 | mpteq2dva 4492 |
. . . . . . . 8
       
 
        coe1                coe1        
         decompPMat
            decompPMat          |
150 | 149 | oveq2d 6311 |
. . . . . . 7
       
 
      g    coe1                coe1               g      decompPMat             decompPMat           |
151 | 150 | mpteq2dva 4492 |
. . . . . 6
   

          g    coe1                coe1                     g      decompPMat             decompPMat            |
152 | 151 | oveq2d 6311 |
. . . . 5
   

     g       g    coe1                coe1                 g       g      decompPMat             decompPMat             |
153 | 109, 135,
152 | 3eqtrd 2491 |
. . . 4
   

               decompPMat     g       g      decompPMat             decompPMat             |
154 | 14, 105, 153 | 3eqtr4rd 2498 |
. . 3
   

               decompPMat       g        decompPMat         decompPMat           |
155 | 154 | ralrimivva 2811 |
. 2
  

  
           decompPMat       g        decompPMat         decompPMat           |
156 | 44, 15 | pmatring 19729 |
. . . . . . 7
 

  |
157 | 21, 156 | syl 17 |
. . . . . 6
  
 
  |
158 | | simprl 765 |
. . . . . 6
  
 
  |
159 | | simprr 767 |
. . . . . 6
  
 
  |
160 | | eqid 2453 |
. . . . . . 7
         |
161 | 16, 160 | ringcl 17806 |
. . . . . 6
 
           |
162 | 157, 158,
159, 161 | syl3anc 1269 |
. . . . 5
  
 
          |
163 | 162 | 3adant3 1029 |
. . . 4
  

           |
164 | 44, 15, 16, 23, 45 | decpmatcl 19803 |
. . . 4
                    decompPMat        |
165 | 163, 164 | syld3an2 1316 |
. . 3
  

          decompPMat        |
166 | 23 | matring 19480 |
. . . . . 6
 

  |
167 | 22, 166 | syl 17 |
. . . . 5
  

   |
168 | | ringcmn 17823 |
. . . . 5

CMnd |
169 | 167, 168 | syl 17 |
. . . 4
  

 CMnd |
170 | | fzfid 12193 |
. . . 4
  

       |
171 | 167 | adantr 467 |
. . . . . 6
   

        |
172 | 33 | adantr 467 |
. . . . . . . 8
   

        |
173 | | simpl2l 1062 |
. . . . . . . 8
   

        |
174 | 41 | adantl 468 |
. . . . . . . 8
   

        |
175 | 172, 173,
174 | 3jca 1189 |
. . . . . . 7
   

      
   |
176 | 175, 46 | syl 17 |
. . . . . 6
   

       decompPMat        |
177 | | simpl2r 1063 |
. . . . . . . 8
   

        |
178 | 52 | adantl 468 |
. . . . . . . 8
   

      
   |
179 | 172, 177,
178 | 3jca 1189 |
. . . . . . 7
   

      

    |
180 | 179, 55 | syl 17 |
. . . . . 6
   

       decompPMat          |
181 | | eqid 2453 |
. . . . . . 7
         |
182 | 45, 181 | ringcl 17806 |
. . . . . 6
   decompPMat       decompPMat
         
decompPMat         decompPMat
          |
183 | 171, 176,
180, 182 | syl3anc 1269 |
. . . . 5
   

       
decompPMat         decompPMat
          |
184 | 183 | ralrimiva 2804 |
. . . 4
  

         decompPMat         decompPMat           |
185 | 45, 169, 170, 184 | gsummptcl 17611 |
. . 3
  

  g        decompPMat         decompPMat             |
186 | 23, 45 | eqmat 19461 |
. . 3
           decompPMat
    
 g        decompPMat
        decompPMat                      decompPMat
  g        decompPMat         decompPMat        
           decompPMat       g        decompPMat         decompPMat            |
187 | 165, 185,
186 | syl2anc 667 |
. 2
  

           decompPMat   g        decompPMat         decompPMat      


           decompPMat
      g        decompPMat         decompPMat            |
188 | 155, 187 | mpbird 236 |
1
  

          decompPMat   g        decompPMat         decompPMat         |