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

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 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
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 ‘ 𝑃 )