Metamath Proof Explorer

Theorem ply1val

Description: The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses ply1val.1 
|- P = ( Poly1 ` R )
ply1val.2 
|- S = ( PwSer1 ` R )
Assertion ply1val 
|- P = ( S |`s ( Base ` ( 1o mPoly R ) ) )

Proof

Step Hyp Ref Expression
1 ply1val.1 
 |-  P = ( Poly1 ` R )
2 ply1val.2 
 |-  S = ( PwSer1 ` R )
3 fveq2 
 |-  ( r = R -> ( PwSer1 ` r ) = ( PwSer1 ` R ) )
4 3 2 eqtr4di 
 |-  ( r = R -> ( PwSer1 ` r ) = S )
5 oveq2 
 |-  ( r = R -> ( 1o mPoly r ) = ( 1o mPoly R ) )
6 5 fveq2d 
 |-  ( r = R -> ( Base ` ( 1o mPoly r ) ) = ( Base ` ( 1o mPoly R ) ) )
7 4 6 oveq12d 
 |-  ( r = R -> ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) ) = ( S |`s ( Base ` ( 1o mPoly R ) ) ) )
8 df-ply1 
 |-  Poly1 = ( r e. _V |-> ( ( PwSer1 ` r ) |`s ( Base ` ( 1o mPoly r ) ) ) )
9 ovex 
 |-  ( S |`s ( Base ` ( 1o mPoly R ) ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( R e. _V -> ( Poly1 ` R ) = ( S |`s ( Base ` ( 1o mPoly R ) ) ) )
11 fvprc 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = (/) )
12 ress0 
 |-  ( (/) |`s ( Base ` ( 1o mPoly R ) ) ) = (/)
13 11 12 eqtr4di 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = ( (/) |`s ( Base ` ( 1o mPoly R ) ) ) )
14 fvprc 
 |-  ( -. R e. _V -> ( PwSer1 ` R ) = (/) )
15 2 14 syl5eq 
 |-  ( -. R e. _V -> S = (/) )
16 15 oveq1d 
 |-  ( -. R e. _V -> ( S |`s ( Base ` ( 1o mPoly R ) ) ) = ( (/) |`s ( Base ` ( 1o mPoly R ) ) ) )
17 13 16 eqtr4d 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = ( S |`s ( Base ` ( 1o mPoly R ) ) ) )
18 10 17 pm2.61i 
 |-  ( Poly1 ` R ) = ( S |`s ( Base ` ( 1o mPoly R ) ) )
19 1 18 eqtri 
 |-  P = ( S |`s ( Base ` ( 1o mPoly R ) ) )