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 e. ( Poly ` S ) -> ( CC _D F ) e. ( Poly ` CC ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnring | |- CCfld e. Ring |
|
| 2 | cnfldbas | |- CC = ( Base ` CCfld ) |
|
| 3 | 2 | subrgid | |- ( CCfld e. Ring -> CC e. ( SubRing ` CCfld ) ) |
| 4 | 1 3 | ax-mp | |- CC e. ( SubRing ` CCfld ) |
| 5 | plyssc | |- ( Poly ` S ) C_ ( Poly ` CC ) |
|
| 6 | 5 | sseli | |- ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) ) |
| 7 | dvply2g | |- ( ( CC e. ( SubRing ` CCfld ) /\ F e. ( Poly ` CC ) ) -> ( CC _D F ) e. ( Poly ` CC ) ) |
|
| 8 | 4 6 7 | sylancr | |- ( F e. ( Poly ` S ) -> ( CC _D F ) e. ( Poly ` CC ) ) |