Definition df-psd

Description: Define the differentiation operation on multivariate polynomials. ( ( ( I mPSDer R )X )F ) is the partial derivative of the polynomial F with respect to X . (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	df-psd	⊢ mPSDer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsd	⊢ mPSDer
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		vx	⊢ 𝑥
5	1	cv	⊢ 𝑖
6		vf	⊢ 𝑓
7		cbs	⊢ Base
8		cmps	⊢ mPwSer
9	3	cv	⊢ 𝑟
10	5 9 8	co	⊢ ( 𝑖 mPwSer 𝑟 )
11	10 7	cfv	⊢ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) )
12		vk	⊢ 𝑘
13		vh	⊢ ℎ
14		cn0	⊢ ℕ0
15		cmap	⊢ ↑m
16	14 5 15	co	⊢ ( ℕ0 ↑m 𝑖 )
17	13	cv	⊢ ℎ
18	17	ccnv	⊢ ◡ ℎ
19		cn	⊢ ℕ
20	18 19	cima	⊢ ( ◡ ℎ “ ℕ )
21		cfn	⊢ Fin
22	20 21	wcel	⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
23	22 13 16	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
24	12	cv	⊢ 𝑘
25	4	cv	⊢ 𝑥
26	25 24	cfv	⊢ ( 𝑘 ‘ 𝑥 )
27		caddc	⊢ +
28		c1	⊢ 1
29	26 28 27	co	⊢ ( ( 𝑘 ‘ 𝑥 ) + 1 )
30		cmg	⊢ .g
31	9 30	cfv	⊢ ( .g ‘ 𝑟 )
32	6	cv	⊢ 𝑓
33	27	cof	⊢ ∘f +
34		vy	⊢ 𝑦
35	34	cv	⊢ 𝑦
36	35 25	wceq	⊢ 𝑦 = 𝑥
37		cc0	⊢ 0
38	36 28 37	cif	⊢ if ( 𝑦 = 𝑥 , 1 , 0 )
39	34 5 38	cmpt	⊢ ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) )
40	24 39 33	co	⊢ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) )
41	40 32	cfv	⊢ ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) )
42	29 41 31	co	⊢ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) )
43	12 23 42	cmpt	⊢ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) )
44	6 11 43	cmpt	⊢ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) )
45	4 5 44	cmpt	⊢ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) )
46	1 3 2 2 45	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )
47	0 46	wceq	⊢ mPSDer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )