Step 
Hyp 
Ref 
Expression 
1 

ply1val.1 
 P = ( Poly1 ` R ) 
2 

ply1val.2 
 S = ( PwSer1 ` R ) 
3 

ply1bas.u 
 U = ( Base ` P ) 
4 

eqid 
 ( 1o mPoly R ) = ( 1o mPoly R ) 
5 

eqid 
 ( 1o mPwSer R ) = ( 1o mPwSer R ) 
6 

eqid 
 ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) ) 
7 

eqid 
 ( Base ` S ) = ( Base ` S ) 
8 
2 7 5

psr1bas2 
 ( Base ` S ) = ( Base ` ( 1o mPwSer R ) ) 
9 
4 5 6 8

mplbasss 
 ( Base ` ( 1o mPoly R ) ) C_ ( Base ` S ) 
10 
1 2

ply1val 
 P = ( S `s ( Base ` ( 1o mPoly R ) ) ) 
11 
10 7

ressbas2 
 ( ( Base ` ( 1o mPoly R ) ) C_ ( Base ` S ) > ( Base ` ( 1o mPoly R ) ) = ( Base ` P ) ) 
12 
9 11

axmp 
 ( Base ` ( 1o mPoly R ) ) = ( Base ` P ) 
13 
3 12

eqtr4i 
 U = ( Base ` ( 1o mPoly R ) ) 