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

Metamath Proof Explorer

Theorem psr1sca2

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

Ref Expression
Hypothesis psr1lmod.p ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
Assertion psr1sca2 ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )

Proof

Step Hyp Ref Expression
1 psr1lmod.p ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2 fvi ⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
3 1 psr1sca ⊢ ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ 𝑃 ) )
4 2 3 eqtrd ⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 ) )
5 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
6 5 str0 ⊢ ∅ = ( Scalar ‘ ∅ )
7 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
8 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ∅ )
9 1 8 eqtrid ⊢ ( ¬ 𝑅 ∈ V → 𝑃 = ∅ )
10 9 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( Scalar ‘ 𝑃 ) = ( Scalar ‘ ∅ ) )
11 6 7 10 3eqtr4a ⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 ) )
12 4 11 pm2.61i ⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )