This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑃 ) )