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 psdffval.s ⊢ S = I mPwSer R
psdffval.b ⊢ B = Base S
psdffval.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
psdffval.i ⊢ φ → I ∈ V
psdffval.r ⊢ φ → R ∈ W
psdfval.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 psdffval.s ⊢ S = I mPwSer R
2 psdffval.b ⊢ B = Base S
3 psdffval.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
4 psdffval.i ⊢ φ → I ∈ V
5 psdffval.r ⊢ φ → R ∈ W
6 psdfval.x ⊢ φ → X ∈ I
7 psdval.f ⊢ φ → F ∈ B
8 psdcoef.k ⊢ φ → K ∈ D
9 1 2 3 4 5 6 7 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ F = k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0
10 fveq1 ⊢ k = K → k ⁡ X = K ⁡ X
11 10 oveq1d ⊢ k = K → k ⁡ X + 1 = K ⁡ X + 1
12 fvoveq1 ⊢ k = K → F ⁡ k + f y ∈ I ⟼ if y = X 1 0 = F ⁡ K + f y ∈ I ⟼ if y = X 1 0
13 11 12 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
14 13 adantl ⊢ φ ∧ 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
15 ovexd ⊢ φ → K ⁡ X + 1 ⋅ R F ⁡ K + f y ∈ I ⟼ if y = X 1 0 ∈ V
16 9 14 8 15 fvmptd ⊢ φ → I mPSDer R ⁡ X ⁡ F ⁡ K = K ⁡ X + 1 ⋅ R F ⁡ K + f y ∈ I ⟼ if y = X 1 0