Step | Hyp | Ref
| Expression |
1 | | crngring 17791 |
. . 3

  |
2 | | simpll 760 |
. . . 4
    
    |
3 | | simplr 762 |
. . . 4
    
    |
4 | | monmat2matmon.a |
. . . . 5
 Mat   |
5 | | monmat2matmon.k |
. . . . 5
     |
6 | | monmat2matmon.t |
. . . . 5

matToPolyMat   |
7 | | monmat2matmon.p |
. . . . 5
Poly1   |
8 | | monmat2matmon.c |
. . . . 5
 Mat   |
9 | | monmat2matmon.b |
. . . . 5
     |
10 | | monmat2matmon.m2 |
. . . . 5
     |
11 | | monmat2matmon.e2 |
. . . . 5
.g mulGrp    |
12 | | monmat2matmon.y |
. . . . 5
var1   |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | mat2pmatscmxcl 19764 |
. . . 4
    
              |
14 | | monmat2matmon.m1 |
. . . . 5
     |
15 | | monmat2matmon.e1 |
. . . . 5
.g mulGrp    |
16 | | monmat2matmon.x |
. . . . 5
var1   |
17 | | monmat2matmon.q |
. . . . 5
Poly1   |
18 | | monmat2matmon.i |
. . . . 5

pMatToMatPoly   |
19 | 7, 8, 9, 14, 15, 16, 4, 17, 18 | pm2mpfval 19820 |
. . . 4
 
                          g              decompPMat         |
20 | 2, 3, 13, 19 | syl3anc 1268 |
. . 3
    
                 g              decompPMat         |
21 | 1, 20 | sylanl2 657 |
. 2
    
                 g              decompPMat         |
22 | | simpll 760 |
. . . . . . . 8
   


 
     |
23 | | simpr 463 |
. . . . . . . . . 10
    
  
   |
24 | 23 | anim1i 572 |
. . . . . . . . 9
   


 
       |
25 | | df-3an 987 |
. . . . . . . . 9
 

 

   |
26 | 24, 25 | sylibr 216 |
. . . . . . . 8
   


 
 
   |
27 | | eqid 2451 |
. . . . . . . . 9
         |
28 | 7, 8, 4, 5, 27, 11, 12, 10, 6 | monmatcollpw 19803 |
. . . . . . . 8
    
 
           decompPMat             |
29 | 22, 26, 28 | syl2anc 667 |
. . . . . . 7
   


 
            decompPMat             |
30 | 29 | oveq1d 6305 |
. . . . . 6
   


 
             decompPMat         
          |
31 | 1 | a1i 11 |
. . . . . . . . . 10


   |
32 | 31 | anim2d 569 |
. . . . . . . . 9

 
      |
33 | 32 | anim1d 568 |
. . . . . . . 8

    
     
     |
34 | 33 | imdistanri 697 |
. . . . . . 7
   


 
     
     |
35 | | ovif 6373 |
. . . . . . . 8
                               |
36 | 4 | matring 19468 |
. . . . . . . . . . . . . 14
 

  |
37 | 17 | ply1sca 18846 |
. . . . . . . . . . . . . 14

Scalar    |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
 

Scalar    |
39 | 38 | ad2antrr 732 |
. . . . . . . . . . . 12
   
   

Scalar    |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . 11
   
   
        Scalar     |
41 | 40 | oveq1d 6305 |
. . . . . . . . . 10
   
   
      
      Scalar        |
42 | 17 | ply1lmod 18845 |
. . . . . . . . . . . . 13

  |
43 | 36, 42 | syl 17 |
. . . . . . . . . . . 12
 

  |
44 | 43 | ad2antrr 732 |
. . . . . . . . . . 11
   
   

  |
45 | 17 | ply1ring 18841 |
. . . . . . . . . . . . . . 15

  |
46 | 36, 45 | syl 17 |
. . . . . . . . . . . . . 14
 

  |
47 | | eqid 2451 |
. . . . . . . . . . . . . . 15
mulGrp  mulGrp   |
48 | 47 | ringmgp 17786 |
. . . . . . . . . . . . . 14

mulGrp    |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . 13
 
 mulGrp    |
50 | 49 | ad2antrr 732 |
. . . . . . . . . . . 12
   
   
 mulGrp    |
51 | | simpr 463 |
. . . . . . . . . . . 12
   
   
   |
52 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
53 | 16, 17, 52 | vr1cl 18810 |
. . . . . . . . . . . . . 14

      |
54 | 36, 53 | syl 17 |
. . . . . . . . . . . . 13
 

      |
55 | 54 | ad2antrr 732 |
. . . . . . . . . . . 12
   
   

      |
56 | 47, 52 | mgpbas 17729 |
. . . . . . . . . . . . 13
       mulGrp    |
57 | 56, 15 | mulgnn0cl 16774 |
. . . . . . . . . . . 12
  mulGrp 
    
        |
58 | 50, 51, 55, 57 | syl3anc 1268 |
. . . . . . . . . . 11
   
   
         |
59 | | eqid 2451 |
. . . . . . . . . . . 12
Scalar  Scalar   |
60 | | eqid 2451 |
. . . . . . . . . . . 12
   Scalar      Scalar    |
61 | | eqid 2451 |
. . . . . . . . . . . 12
         |
62 | 52, 59, 14, 60, 61 | lmod0vs 18124 |
. . . . . . . . . . 11
  
          Scalar            |
63 | 44, 58, 62 | syl2anc 667 |
. . . . . . . . . 10
   
   
     Scalar            |
64 | 41, 63 | eqtrd 2485 |
. . . . . . . . 9
   
   
      
        |
65 | 64 | ifeq2d 3900 |
. . . . . . . 8
   
   
                      
          |
66 | 35, 65 | syl5eq 2497 |
. . . . . . 7
   
   
                             |
67 | 34, 66 | syl 17 |
. . . . . 6
   


 
                             |
68 | 30, 67 | eqtrd 2485 |
. . . . 5
   


 
             decompPMat                    |
69 | 68 | mpteq2dva 4489 |
. . . 4
    
               decompPMat  
        
           |
70 | 69 | oveq2d 6306 |
. . 3
    
   g              decompPMat        g                   |
71 | | ringmnd 17789 |
. . . . . . 7

  |
72 | 46, 71 | syl 17 |
. . . . . 6
 

  |
73 | 72 | adantr 467 |
. . . . 5
    
    |
74 | | nn0ex 10875 |
. . . . . 6
 |
75 | 74 | a1i 11 |
. . . . 5
    
    |
76 | | simprr 766 |
. . . . 5
    
    |
77 | | eqid 2451 |
. . . . 5

    
         
    
          |
78 | 38 | fveq2d 5869 |
. . . . . . . . . . . . 13
 
        Scalar     |
79 | 5, 78 | syl5eq 2497 |
. . . . . . . . . . . 12
 

   Scalar     |
80 | 79 | eleq2d 2514 |
. . . . . . . . . . 11
 
     Scalar      |
81 | 80 | biimpcd 228 |
. . . . . . . . . 10
       Scalar      |
82 | 81 | adantr 467 |
. . . . . . . . 9
 
  

   Scalar      |
83 | 82 | impcom 432 |
. . . . . . . 8
    
     Scalar     |
84 | 83 | adantr 467 |
. . . . . . 7
   
   

   Scalar     |
85 | | eqid 2451 |
. . . . . . . 8
   Scalar      Scalar    |
86 | 52, 59, 14, 85 | lmodvscl 18108 |
. . . . . . 7
     Scalar           
        |
87 | 44, 84, 58, 86 | syl3anc 1268 |
. . . . . 6
   
   
  
        |
88 | 87 | ralrimiva 2802 |
. . . . 5
    
             |
89 | 61, 73, 75, 76, 77, 88 | gsummpt1n0 17597 |
. . . 4
    
   g                   ![]_ ]_](_urbrack.gif)  
    |
90 | 1, 89 | sylanl2 657 |
. . 3
    
   g                   ![]_ ]_](_urbrack.gif)  
    |
91 | 70, 90 | eqtrd 2485 |
. 2
    
   g              decompPMat         ![]_ ]_](_urbrack.gif)       |
92 | | csbov2g 6328 |
. . . 4

  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif) 
    |
93 | | csbov1g 6327 |
. . . . . 6

  ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)    |
94 | | csbvarg 3792 |
. . . . . . 7

  ![]_ ]_](_urbrack.gif)   |
95 | 94 | oveq1d 6305 |
. . . . . 6

   ![]_ ]_](_urbrack.gif)  
   |
96 | 93, 95 | eqtrd 2485 |
. . . . 5

  ![]_ ]_](_urbrack.gif) 
     |
97 | 96 | oveq2d 6306 |
. . . 4

   ![]_ ]_](_urbrack.gif)          |
98 | 92, 97 | eqtrd 2485 |
. . 3

  ![]_ ]_](_urbrack.gif)           |
99 | 98 | ad2antll 735 |
. 2
    
    ![]_ ]_](_urbrack.gif)           |
100 | 21, 91, 99 | 3eqtrd 2489 |
1
    
                      |