Metamath Proof Explorer

Theorem ply1sca2

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypothesis ply1lmod.p 
|- P = ( Poly1 ` R )
Assertion ply1sca2 
|- ( _I ` R ) = ( Scalar ` P )

Proof

Step Hyp Ref Expression
1 ply1lmod.p 
 |-  P = ( Poly1 ` R )
2 fvi 
 |-  ( R e. _V -> ( _I ` R ) = R )
3 1 ply1sca 
 |-  ( R e. _V -> R = ( Scalar ` P ) )
4 2 3 eqtrd 
 |-  ( R e. _V -> ( _I ` R ) = ( Scalar ` P ) )
5 fvprc 
 |-  ( -. R e. _V -> ( _I ` R ) = (/) )
6 fvprc 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = (/) )
7 6 fveq2d 
 |-  ( -. R e. _V -> ( Scalar ` ( Poly1 ` R ) ) = ( Scalar ` (/) ) )
8 1 fveq2i 
 |-  ( Scalar ` P ) = ( Scalar ` ( Poly1 ` R ) )
9 df-sca 
 |-  Scalar = Slot 5
10 9 str0 
 |-  (/) = ( Scalar ` (/) )
11 7 8 10 3eqtr4g 
 |-  ( -. R e. _V -> ( Scalar ` P ) = (/) )
12 5 11 eqtr4d 
 |-  ( -. R e. _V -> ( _I ` R ) = ( Scalar ` P ) )
13 4 12 pm2.61i 
 |-  ( _I ` R ) = ( Scalar ` P )