Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-psd Structured version   Visualization version   GIF version

Definition df-psd 20790
 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 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
Distinct variable group:   𝑓,,𝑖,𝑘,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-psd
StepHypRef Expression
1 cpsd 20786 . 2 class mPSDer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3444 . . 3 class V
5 vx . . . 4 setvar 𝑥
62cv 1537 . . . 4 class 𝑖
7 vf . . . . 5 setvar 𝑓
83cv 1537 . . . . . . 7 class 𝑟
9 cmps 20593 . . . . . . 7 class mPwSer
106, 8, 9co 7139 . . . . . 6 class (𝑖 mPwSer 𝑟)
11 cbs 16479 . . . . . 6 class Base
1210, 11cfv 6328 . . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13 vk . . . . . 6 setvar 𝑘
14 vh . . . . . . . . . . 11 setvar
1514cv 1537 . . . . . . . . . 10 class
1615ccnv 5522 . . . . . . . . 9 class
17 cn 11629 . . . . . . . . 9 class
1816, 17cima 5526 . . . . . . . 8 class ( “ ℕ)
19 cfn 8496 . . . . . . . 8 class Fin
2018, 19wcel 2112 . . . . . . 7 wff ( “ ℕ) ∈ Fin
21 cn0 11889 . . . . . . . 8 class 0
22 cmap 8393 . . . . . . . 8 class m
2321, 6, 22co 7139 . . . . . . 7 class (ℕ0m 𝑖)
2420, 14, 23crab 3113 . . . . . 6 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
255cv 1537 . . . . . . . . 9 class 𝑥
2613cv 1537 . . . . . . . . 9 class 𝑘
2725, 26cfv 6328 . . . . . . . 8 class (𝑘𝑥)
28 c1 10531 . . . . . . . 8 class 1
29 caddc 10533 . . . . . . . 8 class +
3027, 28, 29co 7139 . . . . . . 7 class ((𝑘𝑥) + 1)
31 vy . . . . . . . . . 10 setvar 𝑦
3231, 5weq 1964 . . . . . . . . . . 11 wff 𝑦 = 𝑥
33 cc0 10530 . . . . . . . . . . 11 class 0
3432, 28, 33cif 4428 . . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
3531, 6, 34cmpt 5113 . . . . . . . . 9 class (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
3629cof 7391 . . . . . . . . 9 class f +
3726, 35, 36co 7139 . . . . . . . 8 class (𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
387cv 1537 . . . . . . . 8 class 𝑓
3937, 38cfv 6328 . . . . . . 7 class (𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40 cmg 18220 . . . . . . . 8 class .g
418, 40cfv 6328 . . . . . . 7 class (.g𝑟)
4230, 39, 41co 7139 . . . . . 6 class (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
4313, 24, 42cmpt 5113 . . . . 5 class (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
447, 12, 43cmpt 5113 . . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
455, 6, 44cmpt 5113 . . 3 class (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
462, 3, 4, 4, 45cmpo 7141 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
471, 46wceq 1538 1 wff mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator