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