Metamath Proof Explorer


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 FPolySDFPoly

Proof

Step Hyp Ref Expression
1 cnring fldRing
2 cnfldbas =Basefld
3 2 subrgid fldRingSubRingfld
4 1 3 ax-mp SubRingfld
5 plyssc PolySPoly
6 5 sseli FPolySFPoly
7 dvply2g SubRingfldFPolyDFPoly
8 4 6 7 sylancr FPolySDFPoly