This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) ) ) ) ) )