Definition df-psd 22160

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 22134	. 2 class mPSDer
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3480	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1539	. . . 4 class 𝑖
7		vf	. . . . 5 setvar 𝑓
8	3	cv 1539	. . . . . . 7 class 𝑟
9		cmps 21924	. . . . . . 7 class mPwSer
10	6, 8, 9	co 7431	. . . . . 6 class (𝑖 mPwSer 𝑟)
11		cbs 17247	. . . . . 6 class Base
12	10, 11	cfv 6561	. . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13		vk	. . . . . 6 setvar 𝑘
14		vh	. . . . . . . . . . 11 setvar ℎ
15	14	cv 1539	. . . . . . . . . 10 class ℎ
16	15	ccnv 5684	. . . . . . . . 9 class ◡ℎ
17		cn 12266	. . . . . . . . 9 class ℕ
18	16, 17	cima 5688	. . . . . . . 8 class (◡ℎ “ ℕ)
19		cfn 8985	. . . . . . . 8 class Fin
20	18, 19	wcel 2108	. . . . . . 7 wff (◡ℎ “ ℕ) ∈ Fin
21		cn0 12526	. . . . . . . 8 class ℕ0
22		cmap 8866	. . . . . . . 8 class ↑m
23	21, 6, 22	co 7431	. . . . . . 7 class (ℕ0 ↑m 𝑖)
24	20, 14, 23	crab 3436	. . . . . 6 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
25	5	cv 1539	. . . . . . . . 9 class 𝑥
26	13	cv 1539	. . . . . . . . 9 class 𝑘
27	25, 26	cfv 6561	. . . . . . . 8 class (𝑘‘𝑥)
28		c1 11156	. . . . . . . 8 class 1
29		caddc 11158	. . . . . . . 8 class +
30	27, 28, 29	co 7431	. . . . . . 7 class ((𝑘‘𝑥) + 1)
31		vy	. . . . . . . . . 10 setvar 𝑦
32	31, 5	weq 1962	. . . . . . . . . . 11 wff 𝑦 = 𝑥
33		cc0 11155	. . . . . . . . . . 11 class 0
34	32, 28, 33	cif 4525	. . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
35	31, 6, 34	cmpt 5225	. . . . . . . . 9 class (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
36	29	cof 7695	. . . . . . . . 9 class ∘f +
37	26, 35, 36	co 7431	. . . . . . . 8 class (𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
38	7	cv 1539	. . . . . . . 8 class 𝑓
39	37, 38	cfv 6561	. . . . . . 7 class (𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40		cmg 19085	. . . . . . . 8 class .g
41	8, 40	cfv 6561	. . . . . . 7 class (.g‘𝑟)
42	30, 39, 41	co 7431	. . . . . 6 class (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
43	13, 24, 42	cmpt 5225	. . . . 5 class (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
44	7, 12, 43	cmpt 5225	. . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
45	5, 6, 44	cmpt 5225	. . 3 class (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
46	2, 3, 4, 4, 45	cmpo 7433	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
47	1, 46	wceq 1540	1 wff mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘f + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))

This definition is referenced by:  psdffval  22161