Metamath Proof Explorer

Theorem psr1sca2

Description: Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypothesis psr1lmod.p 
|- P = ( PwSer1 ` R )
Assertion psr1sca2 
|- ( _I ` R ) = ( Scalar ` P )

Proof

Step Hyp Ref Expression
1 psr1lmod.p 
 |-  P = ( PwSer1 ` R )
2 fvi 
 |-  ( R e. _V -> ( _I ` R ) = R )
3 1 psr1sca 
 |-  ( R e. _V -> R = ( Scalar ` P ) )
4 2 3 eqtrd 
 |-  ( R e. _V -> ( _I ` R ) = ( Scalar ` P ) )
5 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
6 5 str0 
 |-  (/) = ( Scalar ` (/) )
7 fvprc 
 |-  ( -. R e. _V -> ( _I ` R ) = (/) )
8 fvprc 
 |-  ( -. R e. _V -> ( PwSer1 ` R ) = (/) )
9 1 8 eqtrid 
 |-  ( -. R e. _V -> P = (/) )
10 9 fveq2d 
 |-  ( -. R e. _V -> ( Scalar ` P ) = ( Scalar ` (/) ) )
11 6 7 10 3eqtr4a 
 |-  ( -. R e. _V -> ( _I ` R ) = ( Scalar ` P ) )
12 4 11 pm2.61i 
 |-  ( _I ` R ) = ( Scalar ` P )