Theorem psdcoef

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

	Ref	Expression
Hypotheses	psdffval.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psdffval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psdffval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	psdffval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psdffval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	psdfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	psdval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	psdcoef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
Assertion	psdcoef	⊢ ( 𝜑 → ( ( ( ( 𝐼 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		psdcoef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
9	1 2 3 4 5 6 7	psdval	⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
10		fveq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) )
11	10	oveq1d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ‘ 𝑋 ) + 1 ) = ( ( 𝐾 ‘ 𝑋 ) + 1 ) )
12		fvoveq1	⊢ ( 𝑘 = 𝐾 → ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
13	11 12	oveq12d	⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
15		ovexd	⊢ ( 𝜑 → ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V )
16	9 14 8 15	fvmptd	⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝐾 ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )