Definition df-psd 19363

Description: Define the differentiation operation on multivariate polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.)

Assertion

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

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

Detailed syntax breakdown of Definition df-psd

Step	Hyp	Ref	Expression
1		cpsd 19359	. 2 class mPSDer
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3173	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1474	. . . 4 class 𝑖
7		vf	. . . . 5 setvar 𝑓
8	3	cv 1474	. . . . . . 7 class 𝑟
9		cmps 19172	. . . . . . 7 class mPwSer
10	6, 8, 9	co 6549	. . . . . 6 class (𝑖 mPwSer 𝑟)
11		cbs 15695	. . . . . 6 class Base
12	10, 11	cfv 5804	. . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13		vk	. . . . . 6 setvar 𝑘
14		vh	. . . . . . . . . . 11 setvar ℎ
15	14	cv 1474	. . . . . . . . . 10 class ℎ
16	15	ccnv 5037	. . . . . . . . 9 class ◡ℎ
17		cn 10897	. . . . . . . . 9 class ℕ
18	16, 17	cima 5041	. . . . . . . 8 class (◡ℎ “ ℕ)
19		cfn 7841	. . . . . . . 8 class Fin
20	18, 19	wcel 1977	. . . . . . 7 wff (◡ℎ “ ℕ) ∈ Fin
21		cn0 11169	. . . . . . . 8 class ℕ0
22		cmap 7744	. . . . . . . 8 class ↑𝑚
23	21, 6, 22	co 6549	. . . . . . 7 class (ℕ0 ↑𝑚 𝑖)
24	20, 14, 23	crab 2900	. . . . . 6 class {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
25	5	cv 1474	. . . . . . . . 9 class 𝑥
26	13	cv 1474	. . . . . . . . 9 class 𝑘
27	25, 26	cfv 5804	. . . . . . . 8 class (𝑘‘𝑥)
28		c1 9816	. . . . . . . 8 class 1
29		caddc 9818	. . . . . . . 8 class +
30	27, 28, 29	co 6549	. . . . . . 7 class ((𝑘‘𝑥) + 1)
31		vy	. . . . . . . . . 10 setvar 𝑦
32	31, 5	weq 1861	. . . . . . . . . . 11 wff 𝑦 = 𝑥
33		cc0 9815	. . . . . . . . . . 11 class 0
34	32, 28, 33	cif 4036	. . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
35	31, 6, 34	cmpt 4643	. . . . . . . . 9 class (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
36	29	cof 6793	. . . . . . . . 9 class ∘𝑓 +
37	26, 35, 36	co 6549	. . . . . . . 8 class (𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
38	7	cv 1474	. . . . . . . 8 class 𝑓
39	37, 38	cfv 5804	. . . . . . 7 class (𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40		cmg 17363	. . . . . . . 8 class .g
41	8, 40	cfv 5804	. . . . . . 7 class (.g‘𝑟)
42	30, 39, 41	co 6549	. . . . . 6 class (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
43	13, 24, 42	cmpt 4643	. . . . 5 class (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
44	7, 12, 43	cmpt 4643	. . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
45	5, 6, 44	cmpt 4643	. . 3 class (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
46	2, 3, 4, 4, 45	cmpt2 6551	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
47	1, 46	wceq 1475	1 wff mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑥) + 1)(.g‘𝑟)(𝑓‘(𝑘 ∘𝑓 + (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))

This definition is referenced by: (None)