Definition df-psd

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

	Ref	Expression
Assertion	df-psd	$$⊢\mathrm{mPSDer}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(x\in i⟼\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsd	$$class\mathrm{mPSDer}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vx	$$setvarx$$
5	1	cv	$$setvari$$
6		vf	$$setvarf$$
7		cbs	$$class\mathrm{Base}$$
8		cmps	$$class\mathrm{mPwSer}$$
9	3	cv	$$setvarr$$
10	5 9 8	co	$$class\left(i\mathrm{mPwSer}r\right)$$
11	10 7	cfv	$$class{\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}$$
12		vk	$$setvark$$
13		vh	$$setvarh$$
14		cn0	$$class{\mathbb{N}}_0$$
15		cmap	$$class{\uparrow }_{𝑚}$$
16	14 5 15	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
17	13	cv	$$setvarh$$
18	17	ccnv	$$class{h}^{-1}$$
19		cn	$$class\mathbb{N}$$
20	18 19	cima	$$class{h}^{-1}\left[\mathbb{N}\right]$$
21		cfn	$$class\mathrm{Fin}$$
22	20 21	wcel	$$wff{h}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
23	22 13 16	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
24	12	cv	$$setvark$$
25	4	cv	$$setvarx$$
26	25 24	cfv	$$classk\left(x\right)$$
27		caddc	$$class+$$
28		c1	$$class1$$
29	26 28 27	co	$$class\left(k\left(x\right)+1\right)$$
30		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
31	9 30	cfv	$$class{\cdot }_r$$
32	6	cv	$$setvarf$$
33	27	cof	$$class{\circ }_f+$$
34		vy	$$setvary$$
35	34	cv	$$setvary$$
36	35 25	wceq	$$wffy=x$$
37		cc0	$$class0$$
38	36 28 37	cif	$$classif\left(y=x,1,0\right)$$
39	34 5 38	cmpt	$$class\left(y\in i⟼if\left(y=x,1,0\right)\right)$$
40	24 39 33	co	$$class\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)$$
41	40 32	cfv	$$classf\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)$$
42	29 41 31	co	$$class\left(\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)$$
43	12 23 42	cmpt	$$class\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)$$
44	6 11 43	cmpt	$$class\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)\right)$$
45	4 5 44	cmpt	$$class\left(x\in i⟼\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)\right)\right)$$
46	1 3 2 2 45	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(x\in i⟼\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)\right)\right)\right)$$
47	0 46	wceq	$$wff\mathrm{mPSDer}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(x\in i⟼\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPwSer}r\right)}⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(x\right)+1\right){\cdot }_{r}f\left(k{+}_f\left(y\in i⟼if\left(y=x,1,0\right)\right)\right)\right)\right)\right)\right)$$