Metamath Proof Explorer

Theorem psdval

Description: Evaluate the partial derivative of a power series. (Contributed by SN, 11-Apr-2025)

Ref Expression
Hypotheses psdffval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdffval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psdffval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psdffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psdffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
psdfval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion psdval ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psdffval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdffval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdffval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
4 psdffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psdffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
6 psdfval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7 psdval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 1 2 3 4 5 6 psdfval ⊢ ( 𝜑 → ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
9 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
10 9 oveq2d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
11 10 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
13 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14 3 13 rabex2 ⊢ 𝐷 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
16 15 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V )
17 8 12 7 16 fvmptd ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )