Step | Hyp | Ref
| Expression |
1 | | coass 5361 |
. . . . 5
    
                                |
2 | | df1o2 7212 |
. . . . . . . . 9
   |
3 | | pf1ind.cb |
. . . . . . . . . 10
     |
4 | | fvex 5889 |
. . . . . . . . . 10
     |
5 | 3, 4 | eqeltri 2545 |
. . . . . . . . 9
 |
6 | | 0ex 4528 |
. . . . . . . . 9
 |
7 | | eqid 2471 |
. . . . . . . . 9
  
              |
8 | 2, 5, 6, 7 | mapsncnv 7536 |
. . . . . . . 8
                |
9 | 8 | coeq2i 5000 |
. . . . . . 7
            
         
             |
10 | 2, 5, 6, 7 | mapsnf1o2 7537 |
. . . . . . . 8
  
            |
11 | | f1ococnv2 5854 |
. . . . . . . 8
              
            
         |
12 | 10, 11 | mp1i 13 |
. . . . . . 7
                       |
13 | 9, 12 | syl5eqr 2519 |
. . . . . 6
                    |
14 | 13 | coeq2d 5002 |
. . . . 5
                        |
15 | 1, 14 | syl5eq 2517 |
. . . 4
                        |
16 | | pf1ind.a |
. . . . 5
   |
17 | | pf1ind.cq |
. . . . . 6
eval1   |
18 | 17, 3 | pf1f 19015 |
. . . . 5
       |
19 | | fcoi1 5769 |
. . . . 5
          |
20 | 16, 18, 19 | 3syl 18 |
. . . 4
      |
21 | 15, 20 | eqtrd 2505 |
. . 3
                     |
22 | | pf1ind.cp |
. . . 4
    |
23 | | pf1ind.ct |
. . . 4
     |
24 | | eqid 2471 |
. . . . . 6
 eval   eval   |
25 | 24, 3 | evlval 18824 |
. . . . 5
 eval    evalSub
     |
26 | 25 | rneqi 5067 |
. . . 4
 eval    evalSub      |
27 | | an4 840 |
. . . . . 6
   
eval              
eval                 eval 
 eval                            |
28 | | eqid 2471 |
. . . . . . . . . . . 12
 eval  
eval   |
29 | 17, 3, 28 | mpfpf1 19016 |
. . . . . . . . . . 11
  eval            |
30 | 17, 3, 28 | mpfpf1 19016 |
. . . . . . . . . . 11
  eval            |
31 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
32 | | pf1ind.wc |
. . . . . . . . . . . . . . . . 17
     |
33 | 31, 32 | elab 3173 |
. . . . . . . . . . . . . . . 16
  
  |
34 | | eleq1 2537 |
. . . . . . . . . . . . . . . 16
        
                |
35 | 33, 34 | syl5bbr 267 |
. . . . . . . . . . . . . . 15
        
              |
36 | 35 | anbi1d 719 |
. . . . . . . . . . . . . 14
        
  
               |
37 | 36 | anbi1d 719 |
. . . . . . . . . . . . 13
        
    
                 |
38 | | ovex 6336 |
. . . . . . . . . . . . . . 15
    |
39 | | pf1ind.we |
. . . . . . . . . . . . . . 15
    
   |
40 | 38, 39 | elab 3173 |
. . . . . . . . . . . . . 14
        |
41 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
        
 
              |
42 | 41 | eleq1d 2533 |
. . . . . . . . . . . . . 14
        
                      |
43 | 40, 42 | syl5bbr 267 |
. . . . . . . . . . . . 13
        
                 |
44 | 37, 43 | imbi12d 327 |
. . . . . . . . . . . 12
        
    
 
                                |
45 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
46 | | pf1ind.wd |
. . . . . . . . . . . . . . . . 17
     |
47 | 45, 46 | elab 3173 |
. . . . . . . . . . . . . . . 16
  
  |
48 | | eleq1 2537 |
. . . . . . . . . . . . . . . 16
        
                |
49 | 47, 48 | syl5bbr 267 |
. . . . . . . . . . . . . . 15
        
              |
50 | 49 | anbi2d 718 |
. . . . . . . . . . . . . 14
        
                                      |
51 | 50 | anbi1d 719 |
. . . . . . . . . . . . 13
        
              
                           |
52 | | oveq2 6316 |
. . . . . . . . . . . . . 14
        
                                |
53 | 52 | eleq1d 2533 |
. . . . . . . . . . . . 13
        
             
                        |
54 | 51, 53 | imbi12d 327 |
. . . . . . . . . . . 12
        
                             
                                                  |
55 | | pf1ind.ad |
. . . . . . . . . . . . . . 15
 
  
      |
56 | 55 | expcom 442 |
. . . . . . . . . . . . . 14
           |
57 | 56 | an4s 842 |
. . . . . . . . . . . . 13
  

   
   |
58 | 57 | expimpd 614 |
. . . . . . . . . . . 12
 
     
   |
59 | 44, 54, 58 | vtocl2ga 3101 |
. . . . . . . . . . 11
                                           
                        |
60 | 29, 30, 59 | syl2an 485 |
. . . . . . . . . 10
   eval   eval                           
                        |
61 | 60 | expcomd 445 |
. . . . . . . . 9
   eval   eval                                                    |
62 | 61 | impcom 437 |
. . . . . . . 8
 
  eval 
 eval                                                   |
63 | 26, 3 | mpff 18833 |
. . . . . . . . . . . 12
  eval          |
64 | 63 | ad2antrl 742 |
. . . . . . . . . . 11
 
  eval 
 eval            |
65 | | ffn 5739 |
. . . . . . . . . . 11
           |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
 
  eval 
 eval        |
67 | 26, 3 | mpff 18833 |
. . . . . . . . . . . 12
  eval          |
68 | 67 | ad2antll 743 |
. . . . . . . . . . 11
 
  eval 
 eval            |
69 | | ffn 5739 |
. . . . . . . . . . 11
           |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
 
  eval 
 eval        |
71 | | eqid 2471 |
. . . . . . . . . . . 12
             |
72 | 2, 5, 6, 71 | mapsnf1o3 7538 |
. . . . . . . . . . 11
             |
73 | | f1of 5828 |
. . . . . . . . . . 11
                           |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . 10
 
  eval 
 eval                  |
75 | | ovex 6336 |
. . . . . . . . . . 11
   |
76 | 75 | a1i 11 |
. . . . . . . . . 10
 
  eval 
 eval        |
77 | 5 | a1i 11 |
. . . . . . . . . 10
 
  eval 
 eval      |
78 | | inidm 3632 |
. . . . . . . . . 10
         |
79 | 66, 70, 74, 76, 76, 77, 78 | ofco 6570 |
. . . . . . . . 9
 
  eval 
 eval                                    |
80 | 79 | eleq1d 2533 |
. . . . . . . 8
 
  eval 
 eval                                          |
81 | 62, 80 | sylibrd 242 |
. . . . . . 7
 
  eval 
 eval                                           |
82 | 81 | expimpd 614 |
. . . . . 6
     eval   eval                                          |
83 | 27, 82 | syl5bi 225 |
. . . . 5
     eval               eval                              |
84 | 83 | imp 436 |
. . . 4
 
   eval               eval                              |
85 | | ovex 6336 |
. . . . . . . . . . . . . . 15
    |
86 | | pf1ind.wf |
. . . . . . . . . . . . . . 15
    
   |
87 | 85, 86 | elab 3173 |
. . . . . . . . . . . . . 14
        |
88 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
        
 
              |
89 | 88 | eleq1d 2533 |
. . . . . . . . . . . . . 14
        
                      |
90 | 87, 89 | syl5bbr 267 |
. . . . . . . . . . . . 13
        
                 |
91 | 37, 90 | imbi12d 327 |
. . . . . . . . . . . 12
        
    
 
                                |
92 | | oveq2 6316 |
. . . . . . . . . . . . . 14
        
                                |
93 | 92 | eleq1d 2533 |
. . . . . . . . . . . . 13
        
             
                        |
94 | 51, 93 | imbi12d 327 |
. . . . . . . . . . . 12
        
                             
                                                  |
95 | | pf1ind.mu |
. . . . . . . . . . . . . . 15
 
  
      |
96 | 95 | expcom 442 |
. . . . . . . . . . . . . 14
           |
97 | 96 | an4s 842 |
. . . . . . . . . . . . 13
  

   
   |
98 | 97 | expimpd 614 |
. . . . . . . . . . . 12
 
     
   |
99 | 91, 94, 98 | vtocl2ga 3101 |
. . . . . . . . . . 11
                                           
                        |
100 | 29, 30, 99 | syl2an 485 |
. . . . . . . . . 10
   eval   eval                           
                        |
101 | 100 | expcomd 445 |
. . . . . . . . 9
   eval   eval                                                    |
102 | 101 | impcom 437 |
. . . . . . . 8
 
  eval 
 eval                                                   |
103 | 66, 70, 74, 76, 76, 77, 78 | ofco 6570 |
. . . . . . . . 9
 
  eval 
 eval                                    |
104 | 103 | eleq1d 2533 |
. . . . . . . 8
 
  eval 
 eval                                          |
105 | 102, 104 | sylibrd 242 |
. . . . . . 7
 
  eval 
 eval                                           |
106 | 105 | expimpd 614 |
. . . . . 6
     eval   eval                                          |
107 | 27, 106 | syl5bi 225 |
. . . . 5
     eval               eval                              |
108 | 107 | imp 436 |
. . . 4
 
   eval               eval                              |
109 | | coeq1 4997 |
. . . . 5
                               |
110 | 109 | eleq1d 2533 |
. . . 4
                     
               |
111 | | coeq1 4997 |
. . . . 5
                    
              |
112 | 111 | eleq1d 2533 |
. . . 4
                   
                     |
113 | | coeq1 4997 |
. . . . 5
                   |
114 | 113 | eleq1d 2533 |
. . . 4
           
             |
115 | | coeq1 4997 |
. . . . 5
                   |
116 | 115 | eleq1d 2533 |
. . . 4
           
             |
117 | | coeq1 4997 |
. . . . 5
                         |
118 | 117 | eleq1d 2533 |
. . . 4
                               |
119 | | coeq1 4997 |
. . . . 5
                         |
120 | 119 | eleq1d 2533 |
. . . 4
                               |
121 | | coeq1 4997 |
. . . . 5
          
            
               |
122 | 121 | eleq1d 2533 |
. . . 4
          
                                  |
123 | 17 | pf1rcl 19014 |
. . . . . . . . 9
   |
124 | 16, 123 | syl 17 |
. . . . . . . 8
   |
125 | 124 | adantr 472 |
. . . . . . 7
 
   |
126 | | 1on 7207 |
. . . . . . . . . . . 12
 |
127 | | eqid 2471 |
. . . . . . . . . . . . 13
 mPoly   mPoly   |
128 | 127 | mplassa 18755 |
. . . . . . . . . . . 12
 
  mPoly
 AssAlg |
129 | 126, 124,
128 | sylancr 676 |
. . . . . . . . . . 11
  mPoly
 AssAlg |
130 | | eqid 2471 |
. . . . . . . . . . . . 13
Poly1  Poly1   |
131 | | eqid 2471 |
. . . . . . . . . . . . 13
algSc Poly1   algSc Poly1    |
132 | 130, 131 | ply1ascl 18928 |
. . . . . . . . . . . 12
algSc Poly1   algSc  mPoly    |
133 | | eqid 2471 |
. . . . . . . . . . . 12
Scalar 
mPoly   Scalar  mPoly    |
134 | 132, 133 | asclrhm 18643 |
. . . . . . . . . . 11
  mPoly  AssAlg algSc Poly1    Scalar  mPoly   RingHom  mPoly     |
135 | 129, 134 | syl 17 |
. . . . . . . . . 10
 algSc Poly1    Scalar  mPoly   RingHom  mPoly     |
136 | 126 | a1i 11 |
. . . . . . . . . . . 12
   |
137 | 127, 136,
124 | mplsca 18746 |
. . . . . . . . . . 11
 Scalar 
mPoly     |
138 | 137 | oveq1d 6323 |
. . . . . . . . . 10
  RingHom
 mPoly    Scalar  mPoly   RingHom  mPoly     |
139 | 135, 138 | eleqtrrd 2552 |
. . . . . . . . 9
 algSc Poly1    RingHom  mPoly     |
140 | | eqid 2471 |
. . . . . . . . . 10
    mPoly
      mPoly
   |
141 | 3, 140 | rhmf 18032 |
. . . . . . . . 9
 algSc Poly1    RingHom  mPoly   algSc Poly1           mPoly     |
142 | 139, 141 | syl 17 |
. . . . . . . 8
 algSc Poly1           mPoly     |
143 | 142 | ffvelrnda 6037 |
. . . . . . 7
 
  algSc Poly1          mPoly
    |
144 | | eqid 2471 |
. . . . . . . 8
eval1  eval1   |
145 | 144, 24, 3, 127, 140 | evl1val 18994 |
. . . . . . 7
   algSc Poly1          mPoly
    eval1     algSc Poly1          eval     algSc Poly1                |
146 | 125, 143,
145 | syl2anc 673 |
. . . . . 6
 
  eval1     algSc Poly1          eval     algSc Poly1                |
147 | 144, 130,
3, 131 | evl1sca 18999 |
. . . . . . 7
    eval1     algSc Poly1             |
148 | 124, 147 | sylan 479 |
. . . . . 6
 
  eval1     algSc Poly1             |
149 | 3 | ressid 15262 |
. . . . . . . . . . . . . 14

 ↾s    |
150 | 125, 149 | syl 17 |
. . . . . . . . . . . . 13
 
  ↾s    |
151 | 150 | oveq2d 6324 |
. . . . . . . . . . . 12
 
  mPoly 
↾s    mPoly
   |
152 | 151 | fveq2d 5883 |
. . . . . . . . . . 11
 
 algSc  mPoly
 ↾s    algSc  mPoly     |
153 | 152, 132 | syl6eqr 2523 |
. . . . . . . . . 10
 
 algSc  mPoly
 ↾s    algSc Poly1     |
154 | 153 | fveq1d 5881 |
. . . . . . . . 9
 
  algSc  mPoly  ↾s        algSc Poly1        |
155 | 154 | fveq2d 5883 |
. . . . . . . 8
 
   eval
    algSc  mPoly 
↾s          eval     algSc Poly1         |
156 | | eqid 2471 |
. . . . . . . . 9
 mPoly 
↾s    mPoly
 ↾s    |
157 | | eqid 2471 |
. . . . . . . . 9
 ↾s   ↾s   |
158 | | eqid 2471 |
. . . . . . . . 9
algSc 
mPoly  ↾s    algSc  mPoly  ↾s     |
159 | 126 | a1i 11 |
. . . . . . . . 9
 
   |
160 | | crngring 17869 |
. . . . . . . . . . 11

  |
161 | 3 | subrgid 18088 |
. . . . . . . . . . 11

SubRing    |
162 | 124, 160,
161 | 3syl 18 |
. . . . . . . . . 10
 SubRing    |
163 | 162 | adantr 472 |
. . . . . . . . 9
 
 SubRing    |
164 | | simpr 468 |
. . . . . . . . 9
 
   |
165 | 25, 156, 157, 3, 158, 159, 125, 163, 164 | evlssca 18822 |
. . . . . . . 8
 
   eval
    algSc  mPoly 
↾s                |
166 | 155, 165 | eqtr3d 2507 |
. . . . . . 7
 
   eval
    algSc Poly1         
     |
167 | 166 | coeq1d 5001 |
. . . . . 6
 
    eval     algSc Poly1                 
            |
168 | 146, 148,
167 | 3eqtr3d 2513 |
. . . . 5
 
                     |
169 | | pf1ind.co |
. . . . . . . 8
 
   |
170 | | snex 4641 |
. . . . . . . . . 10
   |
171 | 5, 170 | xpex 6614 |
. . . . . . . . 9
     |
172 | | pf1ind.wa |
. . . . . . . . 9
     
   |
173 | 171, 172 | elab 3173 |
. . . . . . . 8
         |
174 | 169, 173 | sylibr 217 |
. . . . . . 7
 
         |
175 | 174 | ralrimiva 2809 |
. . . . . 6
  
       |
176 | | sneq 3969 |
. . . . . . . . 9
       |
177 | 176 | xpeq2d 4863 |
. . . . . . . 8
           |
178 | 177 | eleq1d 2533 |
. . . . . . 7
                 |
179 | 178 | rspccva 3135 |
. . . . . 6
   
    

        |
180 | 175, 179 | sylan 479 |
. . . . 5
 
         |
181 | 168, 180 | eqeltrrd 2550 |
. . . 4
 
    
              |
182 | | pf1ind.pr |
. . . . . . . 8
   |
183 | | resiexg 6748 |
. . . . . . . . . 10
    |
184 | 5, 183 | ax-mp 5 |
. . . . . . . . 9
  |
185 | | pf1ind.wb |
. . . . . . . . 9
  
   |
186 | 184, 185 | elab 3173 |
. . . . . . . 8

     |
187 | 182, 186 | sylibr 217 |
. . . . . . 7
      |
188 | 13, 187 | eqeltrd 2549 |
. . . . . 6
                     |
189 | | el1o 7219 |
. . . . . . . . . 10

  |
190 | | fveq2 5879 |
. . . . . . . . . 10

          |
191 | 189, 190 | sylbi 200 |
. . . . . . . . 9
           |
192 | 191 | mpteq2dv 4483 |
. . . . . . . 8
           
       |
193 | 192 | coeq1d 5001 |
. . . . . . 7
                    
              |
194 | 193 | eleq1d 2533 |
. . . . . 6
                   
                     |
195 | 188, 194 | syl5ibrcom 230 |
. . . . 5
                       |
196 | 195 | imp 436 |
. . . 4
 

                    |
197 | 17, 3, 28 | pf1mpf 19017 |
. . . . 5
 
          eval    |
198 | 16, 197 | syl 17 |
. . . 4
            eval    |
199 | 3, 22, 23, 26, 84, 108, 110, 112, 114, 116, 118, 120, 122, 181, 196, 198 | mpfind 18836 |
. . 3
                       |
200 | 21, 199 | eqeltrrd 2550 |
. 2
     |
201 | | pf1ind.wg |
. . . 4
     |
202 | 201 | elabg 3174 |
. . 3
 
 
   |
203 | 16, 202 | syl 17 |
. 2
       |
204 | 200, 203 | mpbid 215 |
1
   |