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		df-sca	|- Scalar = Slot 5
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 )