Theorem dvply2

Description: The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014) (Proof shortened by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Assertion	dvply2	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ℂ D 𝐹 ) ∈ ( Poly ‘ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
3	2	subrgid	⊢ ( ℂfld ∈ Ring → ℂ ∈ ( SubRing ‘ ℂfld ) )
4	1 3	ax-mp	⊢ ℂ ∈ ( SubRing ‘ ℂfld )
5		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
6	5	sseli	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
7		dvply2g	⊢ ( ( ℂ ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ ℂ ) ) → ( ℂ D 𝐹 ) ∈ ( Poly ‘ ℂ ) )
8	4 6 7	sylancr	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ℂ D 𝐹 ) ∈ ( Poly ‘ ℂ ) )