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		df-sca	⊢ Scalar = Slot 5
6	5	str0	⊢ ∅ = ( Scalar ‘ ∅ )
7		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
8		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ∅ )
9	1 8	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑃 = ∅ )
10	9	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Scalar ‘ 𝑃 ) = ( Scalar ‘ ∅ ) )
11	6 7 10	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 ) )
12	4 11	pm2.61i	⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )