Proof of Theorem pmatcollpw3fi1lem1
Step | Hyp | Ref
| Expression |
1 | | simpr 468 |
. . . . 5
   
       g     
            

g     
              |
2 | | pmatcollpw.p |
. . . . . . . . . . 11
Poly1   |
3 | | pmatcollpw.c |
. . . . . . . . . . 11
 Mat   |
4 | 2, 3 | pmatring 19794 |
. . . . . . . . . 10
 

  |
5 | | ringmnd 17867 |
. . . . . . . . . 10

  |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
 

  |
7 | 6 | adantr 472 |
. . . . . . . 8
   
       |
8 | | pmatcollpw.b |
. . . . . . . . 9
     |
9 | | ringcmn 17889 |
. . . . . . . . . . 11

CMnd |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
 

CMnd |
11 | 10 | adantr 472 |
. . . . . . . . 9
   
     CMnd |
12 | | snfi 7668 |
. . . . . . . . . 10
   |
13 | 12 | a1i 11 |
. . . . . . . . 9
   
         |
14 | | simplll 776 |
. . . . . . . . . . 11
   
        
  |
15 | | simpllr 777 |
. . . . . . . . . . 11
   
        
  |
16 | | elmapi 7511 |
. . . . . . . . . . . . 13
             |
17 | 16 | adantl 473 |
. . . . . . . . . . . 12
   
             |
18 | 17 | ffvelrnda 6037 |
. . . . . . . . . . 11
   
               |
19 | | elsni 3985 |
. . . . . . . . . . . . 13
     |
20 | | 0nn0 10908 |
. . . . . . . . . . . . 13
 |
21 | 19, 20 | syl6eqel 2557 |
. . . . . . . . . . . 12
     |
22 | 21 | adantl 473 |
. . . . . . . . . . 11
   
        
  |
23 | | pmatcollpw3.a |
. . . . . . . . . . . 12
 Mat   |
24 | | pmatcollpw3.d |
. . . . . . . . . . . 12
     |
25 | | pmatcollpw.t |
. . . . . . . . . . . 12

matToPolyMat   |
26 | | pmatcollpw.m |
. . . . . . . . . . . 12
     |
27 | | pmatcollpw.e |
. . . . . . . . . . . 12
.g mulGrp    |
28 | | pmatcollpw.x |
. . . . . . . . . . . 12
var1   |
29 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 19841 |
. . . . . . . . . . 11
        
                |
30 | 14, 15, 18, 22, 29 | syl22anc 1293 |
. . . . . . . . . 10
   
                       |
31 | 30 | ralrimiva 2809 |
. . . . . . . . 9
   
                      |
32 | 8, 11, 13, 31 | gsummptcl 17677 |
. . . . . . . 8
   
      g     
              |
33 | | eqid 2471 |
. . . . . . . . 9
       |
34 | | eqid 2471 |
. . . . . . . . 9
         |
35 | 8, 33, 34 | mndrid 16636 |
. . . . . . . 8
  
g     
               g                             g                    |
36 | 7, 32, 35 | syl2anc 673 |
. . . . . . 7
   
       g     
                       g     
              |
37 | | 0z 10972 |
. . . . . . . . . . . . 13
 |
38 | | fzsn 11866 |
. . . . . . . . . . . . 13
         |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
       |
40 | 39 | eqcomi 2480 |
. . . . . . . . . . 11
       |
41 | 40 | a1i 11 |
. . . . . . . . . 10
   
             |
42 | | pmatcollpw3fi1lem1.h |
. . . . . . . . . . . . . . 15
               |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
   
        
                |
44 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
             
   |
45 | 19 | ad2antlr 741 |
. . . . . . . . . . . . . . . . 17
             
   |
46 | 44, 45 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
             
   |
47 | 46 | iftrued 3880 |
. . . . . . . . . . . . . . 15
             
               |
48 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
49 | 48 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
           |
50 | 19, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
             |
51 | 50 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
             
           |
52 | 47, 51 | eqtrd 2505 |
. . . . . . . . . . . . . 14
             
               |
53 | | 1nn0 10909 |
. . . . . . . . . . . . . . . . . . . 20
 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   |
55 | | nn0uz 11217 |
. . . . . . . . . . . . . . . . . . 19
     |
56 | 54, 55 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . 18
       |
57 | | eluzfz1 11832 |
. . . . . . . . . . . . . . . . . 18
    
      |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
59 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
     
       |
60 | 58, 59 | mpbird 240 |
. . . . . . . . . . . . . . . 16
       |
61 | 19, 60 | syl 17 |
. . . . . . . . . . . . . . 15
         |
62 | 61 | adantl 473 |
. . . . . . . . . . . . . 14
   
        
      |
63 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . 18
                 |
64 | 63 | ex 441 |
. . . . . . . . . . . . . . . . 17
      
          |
65 | 16, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
66 | 65 | adantl 473 |
. . . . . . . . . . . . . . 15
   
       
       |
67 | 66 | imp 436 |
. . . . . . . . . . . . . 14
   
               |
68 | 43, 52, 62, 67 | fvmptd 5969 |
. . . . . . . . . . . . 13
   
                   |
69 | 68 | eqcomd 2477 |
. . . . . . . . . . . 12
   
                   |
70 | 69 | fveq2d 5883 |
. . . . . . . . . . 11
   
                           |
71 | 70 | oveq2d 6324 |
. . . . . . . . . 10
   
                                   |
72 | 41, 71 | mpteq12dva 4473 |
. . . . . . . . 9
   
                                         |
73 | 72 | oveq2d 6324 |
. . . . . . . 8
   
      g     
             g       
              |
74 | | ovex 6336 |
. . . . . . . . . . 11
   |
75 | 74 | a1i 11 |
. . . . . . . . . 10
   
         |
76 | 8, 34 | mndidcl 16632 |
. . . . . . . . . . . 12
       |
77 | 6, 76 | syl 17 |
. . . . . . . . . . 11
 
       |
78 | 77 | adantr 472 |
. . . . . . . . . 10
   
           |
79 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
   
        
                |
80 | | 0p1e1 10743 |
. . . . . . . . . . . . . . . . . . . . 21
   |
81 | 80 | eqeq2i 2483 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
82 | | ax-1ne0 9626 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
83 | 82 | neii 2645 |
. . . . . . . . . . . . . . . . . . . . 21
 |
84 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . 21
     |
85 | 83, 84 | mtbiri 310 |
. . . . . . . . . . . . . . . . . . . 20

  |
86 | 81, 85 | sylbi 200 |
. . . . . . . . . . . . . . . . . . 19
  
  |
87 | 86 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
              
  |
88 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . 20
     |
89 | 88 | notbid 301 |
. . . . . . . . . . . . . . . . . . 19
 
   |
90 | 89 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
               
   |
91 | 87, 90 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
              
  |
92 | 91 | iffalsed 3883 |
. . . . . . . . . . . . . . . 16
                      
 |
93 | | pmatcollpw3fi1lem1.0 |
. . . . . . . . . . . . . . . 16
     |
94 | 92, 93 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
                      
      |
95 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
96 | 95, 55 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . . 19
       |
97 | | eluzfz2 11833 |
. . . . . . . . . . . . . . . . . . 19
    
      |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
99 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
     
       |
100 | 98, 99 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
       |
101 | 81, 100 | sylbi 200 |
. . . . . . . . . . . . . . . 16
         |
102 | 101 | adantl 473 |
. . . . . . . . . . . . . . 15
   
        
      |
103 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
     |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . 15
   
        
      |
105 | 79, 94, 102, 104 | fvmptd 5969 |
. . . . . . . . . . . . . 14
   
        
          |
106 | 105 | fveq2d 5883 |
. . . . . . . . . . . . 13
   
        
                  |
107 | 23 | fveq2i 5882 |
. . . . . . . . . . . . . . . 16
        Mat    |
108 | 3 | fveq2i 5882 |
. . . . . . . . . . . . . . . 16
        Mat    |
109 | 25, 2, 107, 108 | 0mat2pmat 19837 |
. . . . . . . . . . . . . . 15
                 |
110 | 109 | ancoms 460 |
. . . . . . . . . . . . . 14
 
               |
111 | 110 | ad2antrr 740 |
. . . . . . . . . . . . 13
   
        
              |
112 | 106, 111 | eqtrd 2505 |
. . . . . . . . . . . 12
   
        
              |
113 | 112 | oveq2d 6324 |
. . . . . . . . . . 11
   
        
 
                    |
114 | 2, 3 | pmatlmod 19795 |
. . . . . . . . . . . . 13
 

  |
115 | 114 | ad2antrr 740 |
. . . . . . . . . . . 12
   
        
  |
116 | | simpllr 777 |
. . . . . . . . . . . . . 14
   
        
  |
117 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
 
   |
118 | 95, 117 | mpbird 240 |
. . . . . . . . . . . . . . . 16
   |
119 | 81, 118 | sylbi 200 |
. . . . . . . . . . . . . . 15
     |
120 | 119 | adantl 473 |
. . . . . . . . . . . . . 14
   
        
  |
121 | | eqid 2471 |
. . . . . . . . . . . . . . 15
mulGrp  mulGrp   |
122 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
123 | 2, 28, 121, 27, 122 | ply1moncl 18941 |
. . . . . . . . . . . . . 14
   
       |
124 | 116, 120,
123 | syl2anc 673 |
. . . . . . . . . . . . 13
   
        
        |
125 | 2 | ply1ring 18918 |
. . . . . . . . . . . . . . . . . 18

  |
126 | 3 | matsca2 19522 |
. . . . . . . . . . . . . . . . . 18
 

Scalar    |
127 | 125, 126 | sylan2 482 |
. . . . . . . . . . . . . . . . 17
 

Scalar    |
128 | 127 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
 
 Scalar    |
129 | 128 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
 
    Scalar         |
130 | 129 | eleq2d 2534 |
. . . . . . . . . . . . . 14
 
       Scalar  
         |
131 | 130 | ad2antrr 740 |
. . . . . . . . . . . . 13
   
        
 
    Scalar  
         |
132 | 124, 131 | mpbird 240 |
. . . . . . . . . . . 12
   
        
     Scalar     |
133 | | eqid 2471 |
. . . . . . . . . . . . 13
Scalar  Scalar   |
134 | | eqid 2471 |
. . . . . . . . . . . . 13
   Scalar      Scalar    |
135 | 133, 26, 134, 34 | lmodvs0 18203 |
. . . . . . . . . . . 12
  
    Scalar                  |
136 | 115, 132,
135 | syl2anc 673 |
. . . . . . . . . . 11
   
        
 
            |
137 | 113, 136 | eqtrd 2505 |
. . . . . . . . . 10
   
        
 
                |
138 | 8, 7, 75, 78, 137 | gsumsnd 17663 |
. . . . . . . . 9
   
      g       
                  |
139 | 138 | eqcomd 2477 |
. . . . . . . 8
   
          g       
              |
140 | 73, 139 | oveq12d 6326 |
. . . . . . 7
   
       g     
                        g       
                  g                       |
141 | 36, 140 | eqtr3d 2507 |
. . . . . 6
   
      g     
              g 
                        g 
                     |
142 | 141 | adantr 472 |
. . . . 5
   
       g     
            
 g                    g 
                        g 
                     |
143 | 1, 142 | eqtrd 2505 |
. . . 4
   
       g     
            
  g       
                  g                       |
144 | 143 | 3impa 1226 |
. . 3
   
     g     
            
  g       
                  g                       |
145 | 20 | a1i 11 |
. . . . 5
   
       |
146 | | simplll 776 |
. . . . . 6
   
            
  |
147 | | simpllr 777 |
. . . . . 6
   
            
  |
148 | | id 22 |
. . . . . . . . . . . . 13
      
        |
149 | | c0ex 9655 |
. . . . . . . . . . . . . . 15
 |
150 | 149 | snid 3988 |
. . . . . . . . . . . . . 14
   |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
      
    |
152 | 148, 151 | ffvelrnd 6038 |
. . . . . . . . . . . 12
      
      |
153 | 16, 152 | syl 17 |
. . . . . . . . . . 11
           |
154 | 153 | ad2antlr 741 |
. . . . . . . . . 10
   
          
      |
155 | 23 | matring 19545 |
. . . . . . . . . . . 12
 

  |
156 | 24, 93 | ring0cl 17880 |
. . . . . . . . . . . 12

  |
157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
 
   |
158 | 157 | ad2antrr 740 |
. . . . . . . . . 10
   
          
  |
159 | 154, 158 | ifcld 3915 |
. . . . . . . . 9
   
          
          |
160 | 159, 42 | fmptd 6061 |
. . . . . . . 8
   
               |
161 | 80 | oveq2i 6319 |
. . . . . . . . 9
           |
162 | 161 | feq2i 5731 |
. . . . . . . 8
          
          |
163 | 160, 162 | sylibr 217 |
. . . . . . 7
   
                 |
164 | 163 | ffvelrnda 6037 |
. . . . . 6
   
            
      |
165 | | elfznn0 11913 |
. . . . . . 7
         |
166 | 165 | adantl 473 |
. . . . . 6
   
            
  |
167 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 19841 |
. . . . . 6
        
                |
168 | 146, 147,
164, 166, 167 | syl22anc 1293 |
. . . . 5
   
            
 
            |
169 | 8, 33, 11, 145, 168 | gsummptfzsplit 17643 |
. . . 4
   
      g                        g                          g 
                     |
170 | 169 | 3adant3 1050 |
. . 3
   
     g     
            
 g                        g                          g 
                     |
171 | 144, 170 | eqtr4d 2508 |
. 2
   
     g     
            

g                        |
172 | | mpteq1 4476 |
. . . 4
                                     
             |
173 | 161, 172 | ax-mp 5 |
. . 3
        
                              |
174 | 173 | oveq2i 6319 |
. 2
 g 
                     g                     |
175 | 171, 174 | syl6eq 2521 |
1
   
     g     
            

g                      |