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

Definition df-psd 20255
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 20251 . 2 class mPSDer
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3492 . . 3 class V
5 vx . . . 4 setvar 𝑥
62cv 1527 . . . 4 class 𝑖
7 vf . . . . 5 setvar 𝑓
83cv 1527 . . . . . . 7 class 𝑟
9 cmps 20059 . . . . . . 7 class mPwSer
106, 8, 9co 7145 . . . . . 6 class (𝑖 mPwSer 𝑟)
11 cbs 16471 . . . . . 6 class Base
1210, 11cfv 6348 . . . . 5 class (Base‘(𝑖 mPwSer 𝑟))
13 vk . . . . . 6 setvar 𝑘
14 vh . . . . . . . . . . 11 setvar
1514cv 1527 . . . . . . . . . 10 class
1615ccnv 5547 . . . . . . . . 9 class
17 cn 11626 . . . . . . . . 9 class
1816, 17cima 5551 . . . . . . . 8 class ( “ ℕ)
19 cfn 8497 . . . . . . . 8 class Fin
2018, 19wcel 2105 . . . . . . 7 wff ( “ ℕ) ∈ Fin
21 cn0 11885 . . . . . . . 8 class 0
22 cmap 8395 . . . . . . . 8 class m
2321, 6, 22co 7145 . . . . . . 7 class (ℕ0m 𝑖)
2420, 14, 23crab 3139 . . . . . 6 class { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin}
255cv 1527 . . . . . . . . 9 class 𝑥
2613cv 1527 . . . . . . . . 9 class 𝑘
2725, 26cfv 6348 . . . . . . . 8 class (𝑘𝑥)
28 c1 10526 . . . . . . . 8 class 1
29 caddc 10528 . . . . . . . 8 class +
3027, 28, 29co 7145 . . . . . . 7 class ((𝑘𝑥) + 1)
31 vy . . . . . . . . . 10 setvar 𝑦
3231, 5weq 1955 . . . . . . . . . . 11 wff 𝑦 = 𝑥
33 cc0 10525 . . . . . . . . . . 11 class 0
3432, 28, 33cif 4463 . . . . . . . . . 10 class if(𝑦 = 𝑥, 1, 0)
3531, 6, 34cmpt 5137 . . . . . . . . 9 class (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
3629cof 7396 . . . . . . . . 9 class f +
3726, 35, 36co 7145 . . . . . . . 8 class (𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))
387cv 1527 . . . . . . . 8 class 𝑓
3937, 38cfv 6348 . . . . . . 7 class (𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))
40 cmg 18162 . . . . . . . 8 class .g
418, 40cfv 6348 . . . . . . 7 class (.g𝑟)
4230, 39, 41co 7145 . . . . . 6 class (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))
4313, 24, 42cmpt 5137 . . . . 5 class (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))
447, 12, 43cmpt 5137 . . . 4 class (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))
455, 6, 44cmpt 5137 . . 3 class (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))))))))
462, 3, 4, 4, 45cmpo 7147 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ (Base‘(𝑖 mPwSer 𝑟)) ↦ (𝑘 ∈ { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ (((𝑘𝑥) + 1)(.g𝑟)(𝑓‘(𝑘f + (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)))))))))
471, 46wceq 1528 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