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	$$⊢F\in \mathrm{Poly}\left(S\right)\to ℂ\mathrm{D}F\in \mathrm{Poly}\left(ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
3	2	subrgid	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1 3	ax-mp	$$⊢ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
5		plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
6	5	sseli	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
7		dvply2g	$$⊢\left(ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge F\in \mathrm{Poly}\left(ℂ\right)\right)\to ℂ\mathrm{D}F\in \mathrm{Poly}\left(ℂ\right)$$
8	4 6 7	sylancr	$$⊢F\in \mathrm{Poly}\left(S\right)\to ℂ\mathrm{D}F\in \mathrm{Poly}\left(ℂ\right)$$