Theorem ply1sca

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

	Ref	Expression
Hypothesis	ply1lmod.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion	ply1sca	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1lmod.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
3	2	psr1sca	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( PwSer1 ‘ 𝑅 ) ) )
4		fvex	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
5	1 2	ply1val	⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
6		eqid	⊢ ( Scalar ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Scalar ‘ ( PwSer1 ‘ 𝑅 ) )
7	5 6	resssca	⊢ ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( Scalar ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Scalar ‘ 𝑃 ) )
8	4 7	ax-mp	⊢ ( Scalar ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Scalar ‘ 𝑃 )
9	3 8	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ 𝑃 ) )