Definition df-psd 19542

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

Assertion

Ref	Expression
df-psd	|- mPSDer = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )

Distinct variable group:   f, h, i, k, r, x, y

Detailed syntax breakdown of Definition df-psd

Step	Hyp	Ref	Expression
1		cpsd 19538	. 2 class mPSDer
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vx	. . . 4 setvar x
6	2	cv 1482	. . . 4 class i
7		vf	. . . . 5 setvar f
8	3	cv 1482	. . . . . . 7 class r
9		cmps 19351	. . . . . . 7 class mPwSer
10	6, 8, 9	co 6650	. . . . . 6 class ( i mPwSer r )
11		cbs 15857	. . . . . 6 class Base
12	10, 11	cfv 5888	. . . . 5 class ( Base ` ( i mPwSer r ) )
13		vk	. . . . . 6 setvar k
14		vh	. . . . . . . . . . 11 setvar h
15	14	cv 1482	. . . . . . . . . 10 class h
16	15	ccnv 5113	. . . . . . . . 9 class `' h
17		cn 11020	. . . . . . . . 9 class NN
18	16, 17	cima 5117	. . . . . . . 8 class ( `' h " NN )
19		cfn 7955	. . . . . . . 8 class Fin
20	18, 19	wcel 1990	. . . . . . 7 wff ( `' h " NN ) e. Fin
21		cn0 11292	. . . . . . . 8 class NN0
22		cmap 7857	. . . . . . . 8 class ^m
23	21, 6, 22	co 6650	. . . . . . 7 class ( NN0 ^m i )
24	20, 14, 23	crab 2916	. . . . . 6 class { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
25	5	cv 1482	. . . . . . . . 9 class x
26	13	cv 1482	. . . . . . . . 9 class k
27	25, 26	cfv 5888	. . . . . . . 8 class ( k ` x )
28		c1 9937	. . . . . . . 8 class 1
29		caddc 9939	. . . . . . . 8 class +
30	27, 28, 29	co 6650	. . . . . . 7 class ( ( k ` x ) + 1 )
31		vy	. . . . . . . . . 10 setvar y
32	31, 5	weq 1874	. . . . . . . . . . 11 wff y = x
33		cc0 9936	. . . . . . . . . . 11 class 0
34	32, 28, 33	cif 4086	. . . . . . . . . 10 class if ( y = x , 1 , 0 )
35	31, 6, 34	cmpt 4729	. . . . . . . . 9 class ( y e. i |-> if ( y = x , 1 , 0 ) )
36	29	cof 6895	. . . . . . . . 9 class oF +
37	26, 35, 36	co 6650	. . . . . . . 8 class ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) )
38	7	cv 1482	. . . . . . . 8 class f
39	37, 38	cfv 5888	. . . . . . 7 class ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) )
40		cmg 17540	. . . . . . . 8 class .g
41	8, 40	cfv 5888	. . . . . . 7 class (.g ` r )
42	30, 39, 41	co 6650	. . . . . 6 class ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) )
43	13, 24, 42	cmpt 4729	. . . . 5 class ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) )
44	7, 12, 43	cmpt 4729	. . . 4 class ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) )
45	5, 6, 44	cmpt 4729	. . 3 class ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) )
46	2, 3, 4, 4, 45	cmpt2 6652	. 2 class ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )
47	1, 46	wceq 1483	1 wff mPSDer = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) (.g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )

This definition is referenced by: (None)