Step | Hyp | Ref
| Expression |
1 | | mplval.p |
. 2
 mPoly   |
2 | | ovex 6342 |
. . . . . 6
 mPwSer   |
3 | 2 | a1i 11 |
. . . . 5
 
  mPwSer    |
4 | | id 22 |
. . . . . . . 8
  mPwSer 

mPwSer    |
5 | | oveq12 6323 |
. . . . . . . 8
 
  mPwSer   mPwSer    |
6 | 4, 5 | sylan9eqr 2517 |
. . . . . . 7
     mPwSer  

mPwSer    |
7 | | mplval.s |
. . . . . . 7
 mPwSer   |
8 | 6, 7 | syl6eqr 2513 |
. . . . . 6
     mPwSer  
  |
9 | 8 | fveq2d 5891 |
. . . . . . . . 9
     mPwSer  
          |
10 | | mplval.b |
. . . . . . . . 9
     |
11 | 9, 10 | syl6eqr 2513 |
. . . . . . . 8
     mPwSer  
      |
12 | | simplr 767 |
. . . . . . . . . . 11
     mPwSer  
  |
13 | 12 | fveq2d 5891 |
. . . . . . . . . 10
     mPwSer  
          |
14 | | mplval.z |
. . . . . . . . . 10
     |
15 | 13, 14 | syl6eqr 2513 |
. . . . . . . . 9
     mPwSer  
     |
16 | 15 | breq2d 4427 |
. . . . . . . 8
     mPwSer  
 finSupp     finSupp   |
17 | 11, 16 | rabeqbidv 3051 |
. . . . . . 7
     mPwSer  
     finSupp       finSupp   |
18 | | mplval.u |
. . . . . . 7

finSupp  |
19 | 17, 18 | syl6eqr 2513 |
. . . . . 6
     mPwSer  
     finSupp        |
20 | 8, 19 | oveq12d 6332 |
. . . . 5
     mPwSer  
 ↾s      finSupp       
↾s    |
21 | 3, 20 | csbied 3401 |
. . . 4
 
   mPwSer   ![]_ ]_](_urbrack.gif) 
↾s     
finSupp        ↾s    |
22 | | df-mpl 18630 |
. . . 4
mPoly    
mPwSer   ![]_ ]_](_urbrack.gif)  ↾s     
finSupp         |
23 | | ovex 6342 |
. . . 4
 ↾s   |
24 | 21, 22, 23 | ovmpt2a 6453 |
. . 3
 
  mPoly   ↾s    |
25 | | reldmmpl 18699 |
. . . . . 6
mPoly |
26 | 25 | ovprc 6344 |
. . . . 5
    mPoly    |
27 | | ress0 15231 |
. . . . 5
 ↾s   |
28 | 26, 27 | syl6eqr 2513 |
. . . 4
    mPoly  
↾s    |
29 | | reldmpsr 18633 |
. . . . . . 7
mPwSer |
30 | 29 | ovprc 6344 |
. . . . . 6
    mPwSer    |
31 | 7, 30 | syl5eq 2507 |
. . . . 5
     |
32 | 31 | oveq1d 6329 |
. . . 4
   
↾s   ↾s    |
33 | 28, 32 | eqtr4d 2498 |
. . 3
    mPoly   ↾s    |
34 | 24, 33 | pm2.61i 169 |
. 2
 mPoly   ↾s   |
35 | 1, 34 | eqtri 2483 |
1

↾s   |