# 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 ) ` (/) )`