Step | Hyp | Ref
| Expression |
1 | | mp2pm2mp.a |
. . 3
 Mat   |
2 | | mp2pm2mp.q |
. . 3
Poly1   |
3 | | mp2pm2mp.l |
. . 3
     |
4 | | mp2pm2mp.m |
. . 3
     |
5 | | mp2pm2mp.e |
. . 3
.g mulGrp    |
6 | | mp2pm2mp.y |
. . 3
var1   |
7 | | mp2pm2mp.i |
. . 3
  
 g      coe1                 |
8 | | mp2pm2mplem2.p |
. . 3
Poly1   |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mp2pm2mplem3 19909 |
. 2
          decompPMat     coe1  g 
    coe1                     |
10 | | eqid 2471 |
. . . . . . . . 9
         |
11 | | eqid 2471 |
. . . . . . . . 9
         |
12 | 8 | ply1ring 18918 |
. . . . . . . . . . . . 13

  |
13 | 12 | 3ad2ant2 1052 |
. . . . . . . . . . . 12
 
   |
14 | | ringcmn 17889 |
. . . . . . . . . . . 12

CMnd |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
 
 CMnd |
16 | 15 | ad3antrrr 744 |
. . . . . . . . . 10
    
   
  coe1           CMnd |
17 | 16 | 3ad2ant1 1051 |
. . . . . . . . 9
     
   
  coe1          
 CMnd |
18 | | simpl2 1034 |
. . . . . . . . . . . . . 14
       |
19 | 18 | ad2antrr 740 |
. . . . . . . . . . . . 13
    
   
  coe1             |
20 | 19 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
     
   
  coe1          
   |
21 | 20 | adantr 472 |
. . . . . . . . . . 11
          
  coe1          
    |
22 | | eqid 2471 |
. . . . . . . . . . . 12
         |
23 | | eqid 2471 |
. . . . . . . . . . . 12
         |
24 | | simpl2 1034 |
. . . . . . . . . . . 12
          
  coe1          
    |
25 | | simpl3 1035 |
. . . . . . . . . . . 12
          
  coe1          
    |
26 | | simpl3 1035 |
. . . . . . . . . . . . . . 15
       |
27 | 26 | ad2antrr 740 |
. . . . . . . . . . . . . 14
    
   
  coe1             |
28 | 27 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
     
   
  coe1          
   |
29 | | eqid 2471 |
. . . . . . . . . . . . . 14
coe1  coe1   |
30 | 29, 3, 2, 23 | coe1fvalcl 18882 |
. . . . . . . . . . . . 13
 
  coe1           |
31 | 28, 30 | sylan 479 |
. . . . . . . . . . . 12
          
  coe1          
   coe1           |
32 | 1, 22, 23, 24, 25, 31 | matecld 19528 |
. . . . . . . . . . 11
          
  coe1          
     coe1             |
33 | | simpr 468 |
. . . . . . . . . . 11
          
  coe1          
    |
34 | | eqid 2471 |
. . . . . . . . . . . 12
mulGrp  mulGrp   |
35 | 22, 8, 6, 4, 34, 5,
10 | ply1tmcl 18942 |
. . . . . . . . . . 11
     coe1          
     coe1                  |
36 | 21, 32, 33, 35 | syl3anc 1292 |
. . . . . . . . . 10
          
  coe1          
      coe1                  |
37 | 36 | ralrimiva 2809 |
. . . . . . . . 9
     
   
  coe1          
      coe1                  |
38 | | simp1lr 1094 |
. . . . . . . . 9
     
   
  coe1          
   |
39 | | oveq 6314 |
. . . . . . . . . . . . . . . . 17
  coe1            coe1                 |
40 | 39 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
  coe1             coe1                            |
41 | | 3simpa 1027 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
   |
42 | 41 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
 
    |
43 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
44 | 1, 43 | mat0op 19521 |
. . . . . . . . . . . . . . . . . . . . . 22
 
              |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
 
             |
46 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . 21
     
   
 

            |
47 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
 
  |
48 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
 
  |
49 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
 
      |
51 | 45, 46, 47, 48, 50 | ovmpt2d 6443 |
. . . . . . . . . . . . . . . . . . . 20
    
   
 
              |
52 | 51 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
   
 

              |
53 | 52 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
     
   
 

                          |
54 | 18 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . 21
     
   
 

  |
55 | 8 | ply1sca 18923 |
. . . . . . . . . . . . . . . . . . . . 21

Scalar    |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     
   
 

Scalar    |
57 | 56 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
     
   
 

       Scalar     |
58 | 57 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
     
   
 

              Scalar          |
59 | 8 | ply1lmod 18922 |
. . . . . . . . . . . . . . . . . . . . 21

  |
60 | 59 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
61 | 60 | ad4antr 746 |
. . . . . . . . . . . . . . . . . . 19
     
   
 

  |
62 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
     
   
 

  |
63 | 8, 6, 34, 5, 10 | ply1moncl 18941 |
. . . . . . . . . . . . . . . . . . . 20
             |
64 | 54, 62, 63 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
     
   
 

          |
65 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
Scalar  Scalar   |
66 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
   Scalar      Scalar    |
67 | 10, 65, 4, 66, 11 | lmod0vs 18202 |
. . . . . . . . . . . . . . . . . . 19
               Scalar              |
68 | 61, 64, 67 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
     
   
 

    Scalar              |
69 | 53, 58, 68 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . 17
     
   
 

                    |
70 | 69 | adantr 472 |
. . . . . . . . . . . . . . . 16
          
 
                      |
71 | 40, 70 | sylan9eqr 2527 |
. . . . . . . . . . . . . . 15
       

  
 
   coe1         
    coe1                  |
72 | 71 | exp31 615 |
. . . . . . . . . . . . . 14
     
   
 


  coe1             coe1                    |
73 | 72 | a2d 28 |
. . . . . . . . . . . . 13
     
   
 

 
 coe1         

    coe1                    |
74 | 73 | ralimdva 2805 |
. . . . . . . . . . . 12
    
   
 
 
  coe1         
 
    coe1                    |
75 | 74 | impancom 447 |
. . . . . . . . . . 11
    
   
  coe1            

 
    coe1                    |
76 | 75 | 3impib 1229 |
. . . . . . . . . 10
     
   
  coe1          
  
    coe1                   |
77 | | breq2 4399 |
. . . . . . . . . . . 12
 
   |
78 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
  coe1      coe1       |
79 | 78 | oveqd 6325 |
. . . . . . . . . . . . . 14
    coe1          coe1         |
80 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
81 | 79, 80 | oveq12d 6326 |
. . . . . . . . . . . . 13
     coe1                coe1              |
82 | 81 | eqeq1d 2473 |
. . . . . . . . . . . 12
      coe1                    coe1                   |
83 | 77, 82 | imbi12d 327 |
. . . . . . . . . . 11
       coe1                

    coe1                    |
84 | 83 | cbvralv 3005 |
. . . . . . . . . 10
 
     coe1                       coe1                   |
85 | 76, 84 | sylibr 217 |
. . . . . . . . 9
     
   
  coe1          
  
    coe1                   |
86 | 10, 11, 17, 37, 38, 85 | gsummptnn0fzv 17694 |
. . . . . . . 8
     
   
  coe1          
  g      coe1               g          coe1                |
87 | 86 | fveq2d 5883 |
. . . . . . 7
     
   
  coe1          
 coe1 
g      coe1               coe1  g          coe1                 |
88 | 87 | fveq1d 5881 |
. . . . . 6
     
   
  coe1          
  coe1  g 
    coe1                   coe1  g          coe1                    |
89 | | simpllr 777 |
. . . . . . . 8
    
   
  coe1             |
90 | 89 | 3ad2ant1 1051 |
. . . . . . 7
     
   
  coe1          
   |
91 | | elfznn0 11913 |
. . . . . . . . . 10
       |
92 | 36 | expcom 442 |
. . . . . . . . . 10

     
   
  coe1          
     coe1                   |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
              
  coe1          
     coe1                   |
94 | 93 | com12 31 |
. . . . . . . 8
     
   
  coe1          
          coe1                   |
95 | 94 | ralrimiv 2808 |
. . . . . . 7
     
   
  coe1          
           coe1                  |
96 | | fzfid 12224 |
. . . . . . 7
     
   
  coe1          
       |
97 | 8, 10, 20, 90, 95, 96 | coe1fzgsumd 18973 |
. . . . . 6
     
   
  coe1          
  coe1  g          coe1                   g       coe1     coe1                    |
98 | 88, 97 | eqtrd 2505 |
. . . . 5
     
   
  coe1          
  coe1  g 
    coe1                   g       coe1     coe1                    |
99 | 98 | mpt2eq3dva 6374 |
. . . 4
    
   
  coe1              coe1  g 
    coe1                      g       coe1     coe1                     |
100 | 18 | 3ad2ant1 1051 |
. . . . . . . . . . 11
   

    |
101 | 100 | adantr 472 |
. . . . . . . . . 10
    
 
        |
102 | | simpl2 1034 |
. . . . . . . . . . 11
    
 
        |
103 | | simpl3 1035 |
. . . . . . . . . . 11
    
 
        |
104 | 26 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
   

    |
105 | 104, 91, 30 | syl2an 485 |
. . . . . . . . . . 11
    
 
       coe1           |
106 | 1, 22, 23, 102, 103, 105 | matecld 19528 |
. . . . . . . . . 10
    
 
         coe1             |
107 | 91 | adantl 473 |
. . . . . . . . . 10
    
 
        |
108 | 43, 22, 8, 6, 4, 34,
5 | coe1tm 18943 |
. . . . . . . . . 10
     coe1          
 coe1     coe1                    coe1                |
109 | 101, 106,
107, 108 | syl3anc 1292 |
. . . . . . . . 9
    
 
      coe1     coe1                    coe1                |
110 | | eqeq1 2475 |
. . . . . . . . . . 11
 
   |
111 | 110 | ifbid 3894 |
. . . . . . . . . 10
       coe1                   coe1               |
112 | 111 | adantl 473 |
. . . . . . . . 9
     
 
             coe1                   coe1               |
113 | | simpl1r 1082 |
. . . . . . . . 9
    
 
        |
114 | | ovex 6336 |
. . . . . . . . . . 11
   coe1        |
115 | 114, 49 | ifex 3940 |
. . . . . . . . . 10
      coe1              |
116 | 115 | a1i 11 |
. . . . . . . . 9
    
 
       
    coe1               |
117 | 109, 112,
113, 116 | fvmptd 5969 |
. . . . . . . 8
    
 
       coe1     coe1                      coe1               |
118 | 117 | mpteq2dva 4482 |
. . . . . . 7
   

        coe1     coe1                            coe1                |
119 | 118 | oveq2d 6324 |
. . . . . 6
   

   g       coe1     coe1                   g            coe1                 |
120 | 119 | mpt2eq3dva 6374 |
. . . . 5
        g       coe1     coe1                      g            coe1                  |
121 | 120 | ad2antrr 740 |
. . . 4
    
   
  coe1              g       coe1     coe1                      g            coe1                  |
122 | | breq2 4399 |
. . . . . . . . . . . . . 14
 
   |
123 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
  coe1      coe1       |
124 | 123 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
   coe1          coe1            |
125 | 122, 124 | imbi12d 327 |
. . . . . . . . . . . . 13
    coe1          
 coe1             |
126 | 125 | rspcva 3134 |
. . . . . . . . . . . 12
   
 coe1           
 coe1            |
127 | 1, 43 | mat0op 19521 |
. . . . . . . . . . . . . . . . . . . . 21
 
              |
128 | 127 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . 20
 
  
           |
129 | 128 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . 19
 
              |
130 | 129 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
   
       coe1           
           |
131 | | elfz2nn0 11911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    

   |
132 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
133 | 132 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   
   |
134 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
135 | 134 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   
   |
136 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
137 | 136 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   
   |
138 | | lelttr 9742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
  
    |
139 | 133, 135,
137, 138 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
       |
140 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
     |
141 | 140 | olcd 400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
       |
142 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
143 | 132 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
   |
144 | | lttri2 9734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
       |
145 | 136, 143,
144 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   
       |
146 | 145 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
   
     |
147 | 142, 146 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
   
     |
148 | 141, 147 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   
  
  |
149 | 148 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   
 
   |
150 | 139, 149 | syld 44 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
   
   |
151 | 150 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
         |
152 | 151 | com24 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
         |
153 | 152 | expimpd 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

          |
154 | 153 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

    
     |
155 | 154 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    


    |
156 | 155 | 3adant2 1049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
    
    |
157 | 131, 156 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        
    |
158 | 157 | com13 82 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

       
    |
159 | 158 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   

    
    |
160 | 159 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
    
   |
161 | 160 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
       coe1              
   |
162 | 161 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

      coe1         

    
   |
163 | 162 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
      coe1         

    
  |
164 | 163 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . . . 22
      
      coe1         

      
    coe1                   |
165 | 164 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . . . . 21
    

      coe1         

           coe1                          |
166 | 165 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
    

      coe1         

 g            coe1                g              |
167 | | ringmnd 17867 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
168 | 167 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
169 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
170 | 43 | gsumz 16699 |
. . . . . . . . . . . . . . . . . . . . . . 23
        g                  |
171 | 168, 169,
170 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  g                  |
172 | 171 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . . . . 21
   
       coe1           g                  |
173 | 172 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
    

      coe1         

 g                  |
174 | 166, 173 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
    

      coe1         

 g            coe1                     |
175 | 174 | mpt2eq3dva 6374 |
. . . . . . . . . . . . . . . . . 18
   
       coe1           
 g            coe1                         |
176 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
   
       coe1           coe1           |
177 | 130, 175,
176 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . . 17
   
       coe1           
 g            coe1                 coe1       |
178 | 177 | ex 441 |
. . . . . . . . . . . . . . . 16
        
  coe1            g            coe1                 coe1        |
179 | 178 | expr 626 |
. . . . . . . . . . . . . . 15
     
    coe1            g            coe1                 coe1         |
180 | 179 | a2d 28 |
. . . . . . . . . . . . . 14
     
  
 coe1          
   g            coe1                 coe1         |
181 | 180 | exp31 615 |
. . . . . . . . . . . . 13

 
     coe1         

   g            coe1                 coe1           |
182 | 181 | com14 90 |
. . . . . . . . . . . 12
   coe1         
 
     
 g            coe1                 coe1           |
183 | 126, 182 | syl 17 |
. . . . . . . . . . 11
   
 coe1                  
 g            coe1                 coe1           |
184 | 183 | ex 441 |
. . . . . . . . . 10

 
  coe1         
 
     
 g            coe1                 coe1            |
185 | 184 | com25 93 |
. . . . . . . . 9


 
      coe1         

   g            coe1                 coe1            |
186 | 185 | pm2.43i 48 |
. . . . . . . 8

 
      coe1         

   g            coe1                 coe1           |
187 | 186 | impcom 437 |
. . . . . . 7
          coe1         

   g            coe1                 coe1          |
188 | 187 | imp31 439 |
. . . . . 6
    
   
  coe1           
   g            coe1                 coe1        |
189 | 188 | com12 31 |
. . . . 5
     
   
  coe1              g            coe1                 coe1        |
190 | 168 | ad3antrrr 744 |
. . . . . . . . . . 11
    
   
  coe1             |
191 | 190 | adantl 473 |
. . . . . . . . . 10
     
   
  coe1           
  |
192 | 191 | 3ad2ant1 1051 |
. . . . . . . . 9
  
   

  
  coe1           
   |
193 | 169 | a1i 11 |
. . . . . . . . 9
  
   

  
  coe1           
       |
194 | | lenlt 9730 |
. . . . . . . . . . . . . . 15
 
     |
195 | 136, 134,
194 | syl2an 485 |
. . . . . . . . . . . . . 14
 
     |
196 | | simpll 768 |
. . . . . . . . . . . . . . . 16
   
   |
197 | | simplr 770 |
. . . . . . . . . . . . . . . 16
   
   |
198 | | simpr 468 |
. . . . . . . . . . . . . . . 16
   
   |
199 | | elfz2nn0 11911 |
. . . . . . . . . . . . . . . 16
    

   |
200 | 196, 197,
198, 199 | syl3anbrc 1214 |
. . . . . . . . . . . . . . 15
   
       |
201 | 200 | ex 441 |
. . . . . . . . . . . . . 14
 
         |
202 | 195, 201 | sylbird 243 |
. . . . . . . . . . . . 13
 
 
       |
203 | 202 | adantll 728 |
. . . . . . . . . . . 12
   

  
       |
204 | 203 | adantr 472 |
. . . . . . . . . . 11
    
   
  coe1           
       |
205 | 204 | impcom 437 |
. . . . . . . . . 10
     
   
  coe1           
      |
206 | 205 | 3ad2ant1 1051 |
. . . . . . . . 9
  
   

  
  coe1           
       |
207 | | eqcom 2478 |
. . . . . . . . . . 11

  |
208 | | ifbi 3893 |
. . . . . . . . . . 11
 
  
    coe1                   coe1               |
209 | 207, 208 | ax-mp 5 |
. . . . . . . . . 10
      coe1                   coe1              |
210 | 209 | mpteq2i 4479 |
. . . . . . . . 9
           coe1                         coe1               |
211 | | simpl2 1034 |
. . . . . . . . . . . 12
       

  
  coe1           

   |
212 | | simpl3 1035 |
. . . . . . . . . . . 12
       

  
  coe1           

   |
213 | 27 | adantl 473 |
. . . . . . . . . . . . . 14
     
   
  coe1           
  |
214 | 213 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
  
   

  
  coe1           
   |
215 | 214, 30 | sylan 479 |
. . . . . . . . . . . 12
       

  
  coe1           

  coe1           |
216 | 1, 22, 23, 211, 212, 215 | matecld 19528 |
. . . . . . . . . . 11
       

  
  coe1           

    coe1             |
217 | 91, 216 | sylan2 482 |
. . . . . . . . . 10
       

  
  coe1           

        coe1             |
218 | 217 | ralrimiva 2809 |
. . . . . . . . 9
  
   

  
  coe1           
          coe1             |
219 | 43, 192, 193, 206, 210, 218 | gsummpt1n0 17675 |
. . . . . . . 8
  
   

  
  coe1           
  g            coe1                 ![]_ ]_](_urbrack.gif)    coe1         |
220 | 219 | mpt2eq3dva 6374 |
. . . . . . 7
     
   
  coe1             
 g            coe1                    ![]_ ]_](_urbrack.gif)    coe1          |
221 | | csbov 6343 |
. . . . . . . . . . . . . . 15
  ![]_ ]_](_urbrack.gif)    coe1           ![]_ ]_](_urbrack.gif)  coe1        |
222 | | csbfv 5916 |
. . . . . . . . . . . . . . . . 17
  ![]_ ]_](_urbrack.gif)  coe1      coe1      |
223 | 222 | a1i 11 |
. . . . . . . . . . . . . . . 16

  ![]_ ]_](_urbrack.gif)  coe1      coe1       |
224 | 223 | oveqd 6325 |
. . . . . . . . . . . . . . 15

    ![]_ ]_](_urbrack.gif)  coe1          coe1         |
225 | 221, 224 | syl5eq 2517 |
. . . . . . . . . . . . . 14

  ![]_ ]_](_urbrack.gif)    coe1          coe1         |
226 | 225 | ad2antlr 741 |
. . . . . . . . . . . . 13
   

    
 ![]_ ]_](_urbrack.gif)    coe1          coe1         |
227 | 226 | mpt2eq3dv 6376 |
. . . . . . . . . . . 12
   

     
  ![]_ ]_](_urbrack.gif)    coe1             coe1          |
228 | | oveq12 6317 |
. . . . . . . . . . . . 13
 
    coe1          coe1         |
229 | 228 | adantl 473 |
. . . . . . . . . . . 12
    
  
 

     coe1          coe1         |
230 | | simprl 772 |
. . . . . . . . . . . 12
   

      |
231 | | simprr 774 |
. . . . . . . . . . . 12
   

      |
232 | | ovex 6336 |
. . . . . . . . . . . . 13
   coe1        |
233 | 232 | a1i 11 |
. . . . . . . . . . . 12
   

       coe1         |
234 | 227, 229,
230, 231, 233 | ovmpt2d 6443 |
. . . . . . . . . . 11
   

          ![]_ ]_](_urbrack.gif)    coe1             coe1         |
235 | 234 | ralrimivva 2814 |
. . . . . . . . . 10
     

   
  ![]_ ]_](_urbrack.gif)    coe1             coe1         |
236 | | simpl1 1033 |
. . . . . . . . . . . 12
       |
237 | 222 | oveqi 6321 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)  coe1          coe1        |
238 | 221, 237 | eqtri 2493 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)    coe1          coe1        |
239 | | simp2 1031 |
. . . . . . . . . . . . . 14
   

    |
240 | | simp3 1032 |
. . . . . . . . . . . . . 14
   

    |
241 | 29, 3, 2, 23 | coe1fvalcl 18882 |
. . . . . . . . . . . . . . . 16
 
  coe1           |
242 | 241 | 3ad2antl3 1194 |
. . . . . . . . . . . . . . 15
      coe1           |
243 | 242 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   

   coe1           |
244 | 1, 22, 23, 239, 240, 243 | matecld 19528 |
. . . . . . . . . . . . 13
   

     coe1             |
245 | 238, 244 | syl5eqel 2553 |
. . . . . . . . . . . 12
   

    ![]_ ]_](_urbrack.gif)    coe1             |
246 | 1, 22, 23, 236, 18, 245 | matbas2d 19525 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)    coe1              |
247 | 1, 23 | eqmat 19526 |
. . . . . . . . . . 11
   
  ![]_ ]_](_urbrack.gif)    coe1           
 coe1               ![]_ ]_](_urbrack.gif)    coe1         coe1      
      ![]_ ]_](_urbrack.gif)    coe1             coe1          |
248 | 246, 242,
247 | syl2anc 673 |
. . . . . . . . . 10
       
  ![]_ ]_](_urbrack.gif)    coe1         coe1      
      ![]_ ]_](_urbrack.gif)    coe1             coe1          |
249 | 235, 248 | mpbird 240 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)    coe1         coe1       |
250 | 249 | ad2antrr 740 |
. . . . . . . 8
    
   
  coe1               ![]_ ]_](_urbrack.gif)    coe1         coe1       |
251 | 250 | adantl 473 |
. . . . . . 7
     
   
  coe1             
  ![]_ ]_](_urbrack.gif)    coe1         coe1       |
252 | 220, 251 | eqtrd 2505 |
. . . . . 6
     
   
  coe1             
 g            coe1                 coe1       |
253 | 252 | ex 441 |
. . . . 5
         
  coe1              g            coe1                 coe1        |
254 | 189, 253 | pm2.61i 169 |
. . . 4
    
   
  coe1              g            coe1                 coe1       |
255 | 99, 121, 254 | 3eqtrd 2509 |
. . 3
    
   
  coe1              coe1  g 
    coe1                    coe1       |
256 | | eqid 2471 |
. . . . . 6
         |
257 | 29, 3, 2, 256 | coe1sfi 18883 |
. . . . 5
 coe1 
finSupp       |
258 | 26, 257 | syl 17 |
. . . 4
     coe1 
finSupp       |
259 | 29, 3, 2, 256, 23 | coe1fsupp 18884 |
. . . . . 6
 coe1         finSupp        |
260 | | elrabi 3181 |
. . . . . 6
 coe1         finSupp      coe1      
   |
261 | 26, 259, 260 | 3syl 18 |
. . . . 5
     coe1      
   |
262 | | fvex 5889 |
. . . . 5
     |
263 | | fsuppmapnn0ub 12245 |
. . . . 5
  coe1      
       coe1  finSupp     
 
 coe1             |
264 | 261, 262,
263 | sylancl 675 |
. . . 4
      coe1  finSupp     
 
 coe1             |
265 | 258, 264 | mpd 15 |
. . 3
       
 coe1            |
266 | 255, 265 | r19.29a 2918 |
. 2
        coe1  g 
    coe1                    coe1       |
267 | 9, 266 | eqtrd 2505 |
1
          decompPMat   coe1       |