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

Metamath Proof Explorer

Theorem psdcoef

Description: Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 psdval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
4 psdval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 psdval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6 psdcoef.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
7 fveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) )
8 7 oveq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ‘ 𝑋 ) + 1 ) = ( ( 𝐾 ‘ 𝑋 ) + 1 ) )
9 fvoveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
10 8 9 oveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
11 1 2 3 4 5 psdval ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
12 ovexd ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V )
13 10 11 6 12 fvmptd4 ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝐾 ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )