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 𝑃 = ( Poly1𝑅 )
Assertion ply1sca2 ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )

Proof

Step Hyp Ref Expression
1 ply1lmod.p 𝑃 = ( Poly1𝑅 )
2 fvi ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
3 1 ply1sca ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ 𝑃 ) )
4 2 3 eqtrd ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 ) )
5 fvprc ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
6 fvprc ( ¬ 𝑅 ∈ V → ( Poly1𝑅 ) = ∅ )
7 6 fveq2d ( ¬ 𝑅 ∈ V → ( Scalar ‘ ( Poly1𝑅 ) ) = ( Scalar ‘ ∅ ) )
8 1 fveq2i ( Scalar ‘ 𝑃 ) = ( Scalar ‘ ( Poly1𝑅 ) )
9 df-sca Scalar = Slot 5
10 9 str0 ∅ = ( Scalar ‘ ∅ )
11 7 8 10 3eqtr4g ( ¬ 𝑅 ∈ V → ( Scalar ‘ 𝑃 ) = ∅ )
12 5 11 eqtr4d ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 ) )
13 4 12 pm2.61i ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )