Definition df-psd 22477

Description: Define the differentiation operation on multivariate polynomials. (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) is the partial derivative of the polynomial 𝐹 with respect to 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.)

Assertion

Ref	Expression
df-psd	⊢ mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))

Distinct variable group:   𝑓,ℎ,𝑖,𝑘,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-psd

Step	Hyp	Ref	Expression
1		cpsd 22455	. 2 class mPSDer
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3450	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1568	. . . 4 class 𝑖
7		vf	. . . . 5 setvar 𝑓
8	3	cv 1568	. . . . . . 7 class 𝑟
9		cmps 22212	. . . . . . 7 class mPwSer
10	6, 8, 9	co 7420	. . . . . 6 class (𝑖 mPwSer 𝑟)
11		cbs 17387	. . . . . 6 class Base
12	10, 11	cfv 6538	. . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13		vk	. . . . . 6 setvar 𝑘
14		vh	. . . . . . . . . . 11 setvar ℎ
15	14	cv 1568	. . . . . . . . . 10 class ℎ
16	15	ccnv 5649	. . . . . . . . 9 class ◡ℎ
17		cn 12335	. . . . . . . . 9 class ℕ
18	16, 17	cima 5653	. . . . . . . 8 class (◡ℎ “ ℕ)
19		cfn 8973	. . . . . . . 8 class Fin
20	18, 19	wcel 2144	. . . . . . 7 wff (◡ℎ “ ℕ) ∈ Fin
21		cn0 12606	. . . . . . . 8 class ℕ0
22		cmap 8847	. . . . . . . 8 class ↑m
23	21, 6, 22	co 7420	. . . . . . 7 class (ℕ0 ↑m 𝑖)
24	20, 14, 23	crab 3412	. . . . . 6 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
25	5	cv 1568	. . . . . . . . 9 class 𝑥
26	13	cv 1568	. . . . . . . . 9 class 𝑘
27	25, 26	cfv 6538	. . . . . . . 8 class (𝑘‘𝑥)
28		c1 11201	. . . . . . . 8 class 1
29		caddc 11203	. . . . . . . 8 class +
30	27, 28, 29	co 7420	. . . . . . 7 class ((𝑘‘𝑥) + 1)
31		vy	. . . . . . . . . 10 setvar 𝑦
32	31, 5	weq 1994	. . . . . . . . . . 11 wff 𝑦 = 𝑥
33		cc0 11200	. . . . . . . . . . 11 class 0
34	32, 28, 33	cif 4481	. . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
35	31, 6, 34	cmpt 5185	. . . . . . . . 9 class (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
36	29	cof 7691	. . . . . . . . 9 class ∘f +
37	26, 35, 36	co 7420	. . . . . . . 8 class (𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
38	7	cv 1568	. . . . . . . 8 class 𝑓
39	37, 38	cfv 6538	. . . . . . 7 class (𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40		cmg 19277	. . . . . . . 8 class .g
41	8, 40	cfv 6538	. . . . . . 7 class (.g‘𝑟)
42	30, 39, 41	co 7420	. . . . . 6 class (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
43	13, 24, 42	cmpt 5185	. . . . 5 class (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
44	7, 12, 43	cmpt 5185	. . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
45	5, 6, 44	cmpt 5185	. . 3 class (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
46	2, 3, 4, 4, 45	cmpo 7422	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
47	1, 46	wceq 1569	1 wff mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))

This definition is used by:  psdffval  22478