Metamath Proof Explorer

Theorem psdval

Description: Evaluate the partial derivative of a power series. (Contributed by SN, 11-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
Assertion psdval ⊢ φ → I mPSDer R ⁡ X ⁡ F = k ∈ D ⟼ 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 1 2 3 4 5 6 psdfval ⊢ φ → I mPSDer R ⁡ X = f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0
9 fveq1 ⊢ f = F → f ⁡ k + f y ∈ I ⟼ if y = X 1 0 = F ⁡ k + f y ∈ I ⟼ if y = X 1 0
10 9 oveq2d ⊢ f = F → 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 10 mpteq2dv ⊢ f = F → k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0 = k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0
12 11 adantl ⊢ φ ∧ f = F → k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0 = k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0
13 ovex ⊢ ℕ 0 I ∈ V
14 3 13 rabex2 ⊢ D ∈ V
15 14 a1i ⊢ φ → D ∈ V
16 15 mptexd ⊢ φ → k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ V
17 8 12 7 16 fvmptd ⊢ φ → I mPSDer R ⁡ X ⁡ F = k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0