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

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
StepHypRef 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 𝑥
62cv 1474 . . . 4 class 𝑖
7 vf . . . . 5 setvar 𝑓
83cv 1474 . . . . . . 7 class 𝑟
9 cmps 19172 . . . . . . 7 class mPwSer
106, 8, 9co 6549 . . . . . 6 class (𝑖 mPwSer 𝑟)
11 cbs 15695 . . . . . 6 class Base
1210, 11cfv 5804 . . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13 vk . . . . . 6 setvar 𝑘
14 vh . . . . . . . . . . 11 setvar
1514cv 1474 . . . . . . . . . 10 class
1615ccnv 5037 . . . . . . . . 9 class
17 cn 10897 . . . . . . . . 9 class
1816, 17cima 5041 . . . . . . . 8 class ( “ ℕ)
19 cfn 7841 . . . . . . . 8 class Fin
2018, 19wcel 1977 . . . . . . 7 wff ( “ ℕ) ∈ Fin
21 cn0 11169 . . . . . . . 8 class 0
22 cmap 7744 . . . . . . . 8 class 𝑚
2321, 6, 22co 6549 . . . . . . 7 class (ℕ0𝑚 𝑖)
2420, 14, 23crab 2900 . . . . . 6 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
255cv 1474 . . . . . . . . 9 class 𝑥
2613cv 1474 . . . . . . . . 9 class 𝑘
2725, 26cfv 5804 . . . . . . . 8 class (𝑘𝑥)
28 c1 9816 . . . . . . . 8 class 1
29 caddc 9818 . . . . . . . 8 class +
3027, 28, 29co 6549 . . . . . . 7 class ((𝑘𝑥) + 1)
31 vy . . . . . . . . . 10 setvar 𝑦
3231, 5weq 1861 . . . . . . . . . . 11 wff 𝑦 = 𝑥
33 cc0 9815 . . . . . . . . . . 11 class 0
3432, 28, 33cif 4036 . . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
3531, 6, 34cmpt 4643 . . . . . . . . 9 class (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
3629cof 6793 . . . . . . . . 9 class 𝑓 +
3726, 35, 36co 6549 . . . . . . . 8 class (𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
387cv 1474 . . . . . . . 8 class 𝑓
3937, 38cfv 5804 . . . . . . 7 class (𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40 cmg 17363 . . . . . . . 8 class .g
418, 40cfv 5804 . . . . . . 7 class (.g𝑟)
4230, 39, 41co 6549 . . . . . 6 class (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
4313, 24, 42cmpt 4643 . . . . 5 class (𝑘 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
447, 12, 43cmpt 4643 . . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
455, 6, 44cmpt 4643 . . 3 class (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
462, 3, 4, 4, 45cmpt2 6551 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
471, 46wceq 1475 1 wff mPSDer = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘𝑓 + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator