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 S = I mPwSer R
psdval.b B = Base S
psdval.d D = h 0 I | h -1 Fin
psdval.x φ X I
psdval.f φ F B
psdcoef.k φ K D
Assertion psdcoef φ I mPSDer R X F K = K X + 1 R F K + f y I if y = X 1 0

Proof

Step Hyp Ref Expression
1 psdval.s S = I mPwSer R
2 psdval.b B = Base S
3 psdval.d D = h 0 I | h -1 Fin
4 psdval.x φ X I
5 psdval.f φ F B
6 psdcoef.k φ K D
7 fveq1 k = K k X = K X
8 7 oveq1d k = K k X + 1 = K X + 1
9 fvoveq1 k = K F k + f y I if y = X 1 0 = F K + f y I if y = X 1 0
10 8 9 oveq12d k = K k X + 1 R F k + f y I if y = X 1 0 = K X + 1 R F K + f y I if y = X 1 0
11 1 2 3 4 5 psdval φ I mPSDer R X F = k D k X + 1 R F k + f y I if y = X 1 0
12 ovexd φ K X + 1 R F K + f y I if y = X 1 0 V
13 10 11 6 12 fvmptd4 φ I mPSDer R X F K = K X + 1 R F K + f y I if y = X 1 0