Metamath Proof Explorer

Theorem psr1val

Description: Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypothesis psr1val.1 
|- S = ( PwSer1 ` R )
Assertion psr1val 
|- S = ( ( 1o ordPwSer R ) ` (/) )

Proof

Step Hyp Ref Expression
1 psr1val.1 
 |-  S = ( PwSer1 ` R )
2 oveq2 
 |-  ( r = R -> ( 1o ordPwSer r ) = ( 1o ordPwSer R ) )
3 2 fveq1d 
 |-  ( r = R -> ( ( 1o ordPwSer r ) ` (/) ) = ( ( 1o ordPwSer R ) ` (/) ) )
4 df-psr1 
 |-  PwSer1 = ( r e. _V |-> ( ( 1o ordPwSer r ) ` (/) ) )
5 fvex 
 |-  ( ( 1o ordPwSer R ) ` (/) ) e. _V
6 3 4 5 fvmpt 
 |-  ( R e. _V -> ( PwSer1 ` R ) = ( ( 1o ordPwSer R ) ` (/) ) )
7 0fv 
 |-  ( (/) ` (/) ) = (/)
8 7 eqcomi 
 |-  (/) = ( (/) ` (/) )
9 fvprc 
 |-  ( -. R e. _V -> ( PwSer1 ` R ) = (/) )
10 reldmopsr 
 |-  Rel dom ordPwSer
11 10 ovprc2 
 |-  ( -. R e. _V -> ( 1o ordPwSer R ) = (/) )
12 11 fveq1d 
 |-  ( -. R e. _V -> ( ( 1o ordPwSer R ) ` (/) ) = ( (/) ` (/) ) )
13 8 9 12 3eqtr4a 
 |-  ( -. R e. _V -> ( PwSer1 ` R ) = ( ( 1o ordPwSer R ) ` (/) ) )
14 6 13 pm2.61i 
 |-  ( PwSer1 ` R ) = ( ( 1o ordPwSer R ) ` (/) )
15 1 14 eqtri 
 |-  S = ( ( 1o ordPwSer R ) ` (/) )