Theorem psr1sca

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

	Ref	Expression
Hypothesis	psr1lmod.p	|- P = ( PwSer1 ` R )
Assertion	psr1sca	|- ( R e. V -> R = ( Scalar ` P ) )

Proof

Step	Hyp	Ref	Expression
1		psr1lmod.p	|- P = ( PwSer1 ` R )
2		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
3	1	psr1val	|- P = ( ( 1o ordPwSer R ) ` (/) )
4		0ss	|- (/) C_ ( 1o X. 1o )
5	4	a1i	|- ( R e. V -> (/) C_ ( 1o X. 1o ) )
6		1on	|- 1o e. On
7	6	a1i	|- ( R e. V -> 1o e. On )
8		id	|- ( R e. V -> R e. V )
9	2 3 5 7 8	opsrsca	|- ( R e. V -> R = ( Scalar ` P ) )