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	$$⊢S=I\mathrm{mPwSer}R$$
	psdval.b	$$⊢B={\mathrm{Base}}_S$$
	psdval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psdval.x	$$⊢\phi \to X\in I$$
	psdval.f	$$⊢\phi \to F\in B$$
	psdcoef.k	$$⊢\phi \to K\in D$$
Assertion	psdcoef	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\left(K\right)=\left(K\left(X\right)+1\right){\cdot }_{R}F\left(K{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psdval.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psdval.b	$$⊢B={\mathrm{Base}}_S$$
3		psdval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
4		psdval.x	$$⊢\phi \to X\in I$$
5		psdval.f	$$⊢\phi \to F\in B$$
6		psdcoef.k	$$⊢\phi \to K\in D$$
7		fveq1	$$⊢k=K\to k\left(X\right)=K\left(X\right)$$
8	7	oveq1d	$$⊢k=K\to k\left(X\right)+1=K\left(X\right)+1$$
9		fvoveq1	$$⊢k=K\to F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=F\left(K{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
10	8 9	oveq12d	$$⊢k=K\to \left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(K\left(X\right)+1\right){\cdot }_{R}F\left(K{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
11	1 2 3 4 5	psdval	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(k\in D⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)$$
12		ovexd	$$⊢\phi \to \left(K\left(X\right)+1\right){\cdot }_{R}F\left(K{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\in \mathrm{V}$$
13	10 11 6 12	fvmptd4	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\left(K\right)=\left(K\left(X\right)+1\right){\cdot }_{R}F\left(K{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$