dvply2g

Description: The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

		Ref	Expression
	Assertion	dvply2g	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to ℂ D F \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
2	1	adantl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F : ℂ ⟶ ℂ$
3	2	feqmptd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F = (a \in ℂ ⟼ F (a))$
4		simplr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land a \in ℂ) \to F \in Poly (S)$
5		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
6	5	adantl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) \in ℕ_{0}$
7	6	nn0zd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) \in ℤ$
8	7	adantr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land a \in ℂ) \to \deg (F) \in ℤ$
9		uzid	$⊢ \deg (F) \in ℤ \to \deg (F) \in ℤ_{\geq \deg (F)}$
10		peano2uz	$⊢ \deg (F) \in ℤ_{\geq \deg (F)} \to \deg (F) + 1 \in ℤ_{\geq \deg (F)}$
11	8 9 10	3syl	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land a \in ℂ) \to \deg (F) + 1 \in ℤ_{\geq \deg (F)}$
12		simpr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land a \in ℂ) \to a \in ℂ$
13		eqid	$⊢ coeff (F) = coeff (F)$
14		eqid	$⊢ \deg (F) = \deg (F)$
15	13 14	coeid3	$⊢ (F \in Poly (S) \land \deg (F) + 1 \in ℤ_{\geq \deg (F)} \land a \in ℂ) \to F (a) = \sum_{b = 0}^{\deg (F) + 1} coeff (F) (b) a^{b}$
16	4 11 12 15	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land a \in ℂ) \to F (a) = \sum_{b = 0}^{\deg (F) + 1} coeff (F) (b) a^{b}$
17	16	mpteq2dva	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (a \in ℂ ⟼ F (a)) = (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F) + 1} coeff (F) (b) a^{b})$
18	3 17	eqtrd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to F = (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F) + 1} coeff (F) (b) a^{b})$
19	6	nn0cnd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) \in ℂ$
20		ax-1cn	$⊢ 1 \in ℂ$
21		pncan	$⊢ (\deg (F) \in ℂ \land 1 \in ℂ) \to \deg (F) + 1 - 1 = \deg (F)$
22	19 20 21	sylancl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) + 1 - 1 = \deg (F)$
23	22	eqcomd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) = \deg (F) + 1 - 1$
24	23	oveq2d	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (0 \dots \deg (F)) = (0 \dots \deg (F) + 1 - 1)$
25	24	sumeq1d	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \sum_{b = 0}^{\deg (F)} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b} = \sum_{b = 0}^{\deg (F) + 1 - 1} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b}$
26	25	mpteq2dv	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F)} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b}) = (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F) + 1 - 1} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b})$
27	13	coef3	$⊢ F \in Poly (S) \to coeff (F) : ℕ_{0} ⟶ ℂ$
28	27	adantl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to coeff (F) : ℕ_{0} ⟶ ℂ$
29		oveq1	$⊢ c = b \to c + 1 = b + 1$
30		fvoveq1	$⊢ c = b \to coeff (F) (c + 1) = coeff (F) (b + 1)$
31	29 30	oveq12d	$⊢ c = b \to (c + 1) coeff (F) (c + 1) = (b + 1) coeff (F) (b + 1)$
32	31	cbvmptv	$⊢ (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) = (b \in ℕ_{0} ⟼ (b + 1) coeff (F) (b + 1))$
33		peano2nn0	$⊢ \deg (F) \in ℕ_{0} \to \deg (F) + 1 \in ℕ_{0}$
34	6 33	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to \deg (F) + 1 \in ℕ_{0}$
35	18 26 28 32 34	dvply1	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to ℂ D F = (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F)} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b})$
36		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
37	36	subrgss	$⊢ S \in SubRing (ℂ_{fld}) \to S \subseteq ℂ$
38	37	adantr	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to S \subseteq ℂ$
39		elfznn0	$⊢ b \in (0 \dots \deg (F)) \to b \in ℕ_{0}$
40		simpll	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to S \in SubRing (ℂ_{fld})$
41		zsssubrg	$⊢ S \in SubRing (ℂ_{fld}) \to ℤ \subseteq S$
42	41	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to ℤ \subseteq S$
43		peano2nn0	$⊢ c \in ℕ_{0} \to c + 1 \in ℕ_{0}$
44	43	adantl	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to c + 1 \in ℕ_{0}$
45	44	nn0zd	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to c + 1 \in ℤ$
46	42 45	sseldd	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to c + 1 \in S$
47		simplr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to F \in Poly (S)$
48		subrgsubg	$⊢ S \in SubRing (ℂ_{fld}) \to S \in SubGrp (ℂ_{fld})$
49		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
50	49	subg0cl	$⊢ S \in SubGrp (ℂ_{fld}) \to 0 \in S$
51	48 50	syl	$⊢ S \in SubRing (ℂ_{fld}) \to 0 \in S$
52	51	ad2antrr	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to 0 \in S$
53	13	coef2	$⊢ (F \in Poly (S) \land 0 \in S) \to coeff (F) : ℕ_{0} ⟶ S$
54	47 52 53	syl2anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to coeff (F) : ℕ_{0} ⟶ S$
55	54 44	ffvelcdmd	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to coeff (F) (c + 1) \in S$
56		mpocnfldmul	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) = \cdot_{ℂ_{fld}}$
57	56	subrgmcl	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to (c + 1) (u \in ℂ, v \in ℂ ⟼ u v) coeff (F) (c + 1) \in S$
58	37	a1d	$⊢ S \in SubRing (ℂ_{fld}) \to (coeff (F) (c + 1) \in S \to S \subseteq ℂ)$
59		ssel	$⊢ S \subseteq ℂ \to (c + 1 \in S \to c + 1 \in ℂ)$
60	59	a1i	$⊢ S \in SubRing (ℂ_{fld}) \to (S \subseteq ℂ \to (c + 1 \in S \to c + 1 \in ℂ))$
61	58 60	syld	$⊢ S \in SubRing (ℂ_{fld}) \to (coeff (F) (c + 1) \in S \to (c + 1 \in S \to c + 1 \in ℂ))$
62	61	com23	$⊢ S \in SubRing (ℂ_{fld}) \to (c + 1 \in S \to (coeff (F) (c + 1) \in S \to c + 1 \in ℂ))$
63	62	3imp	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to c + 1 \in ℂ$
64	37	a1d	$⊢ S \in SubRing (ℂ_{fld}) \to (c + 1 \in S \to S \subseteq ℂ)$
65		ssel	$⊢ S \subseteq ℂ \to (coeff (F) (c + 1) \in S \to coeff (F) (c + 1) \in ℂ)$
66	65	a1i	$⊢ S \in SubRing (ℂ_{fld}) \to (S \subseteq ℂ \to (coeff (F) (c + 1) \in S \to coeff (F) (c + 1) \in ℂ))$
67	64 66	syld	$⊢ S \in SubRing (ℂ_{fld}) \to (c + 1 \in S \to (coeff (F) (c + 1) \in S \to coeff (F) (c + 1) \in ℂ))$
68	67	3imp	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to coeff (F) (c + 1) \in ℂ$
69	63 68	jca	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to (c + 1 \in ℂ \land coeff (F) (c + 1) \in ℂ)$
70		ovmpot	$⊢ (c + 1 \in ℂ \land coeff (F) (c + 1) \in ℂ) \to (c + 1) (u \in ℂ, v \in ℂ ⟼ u v) coeff (F) (c + 1) = (c + 1) coeff (F) (c + 1)$
71	69 70	syl	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to (c + 1) (u \in ℂ, v \in ℂ ⟼ u v) coeff (F) (c + 1) = (c + 1) coeff (F) (c + 1)$
72	71	eleq1d	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to ((c + 1) (u \in ℂ, v \in ℂ ⟼ u v) coeff (F) (c + 1) \in S \leftrightarrow (c + 1) coeff (F) (c + 1) \in S)$
73	57 72	mpbid	$⊢ (S \in SubRing (ℂ_{fld}) \land c + 1 \in S \land coeff (F) (c + 1) \in S) \to (c + 1) coeff (F) (c + 1) \in S$
74	40 46 55 73	syl3anc	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land c \in ℕ_{0}) \to (c + 1) coeff (F) (c + 1) \in S$
75	74	fmpttd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) : ℕ_{0} ⟶ S$
76	75	ffvelcdmda	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land b \in ℕ_{0}) \to (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) \in S$
77	39 76	sylan2	$⊢ ((S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \land b \in (0 \dots \deg (F))) \to (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) \in S$
78	38 6 77	elplyd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to (a \in ℂ ⟼ \sum_{b = 0}^{\deg (F)} (c \in ℕ_{0} ⟼ (c + 1) coeff (F) (c + 1)) (b) a^{b}) \in Poly (S)$
79	35 78	eqeltrd	$⊢ (S \in SubRing (ℂ_{fld}) \land F \in Poly (S)) \to ℂ D F \in Poly (S)$

Metamath Proof Explorer

Theorem dvply2g

Proof