Metamath Proof Explorer

Theorem psdval

Description: Evaluate the partial derivative of a power series. (Contributed by SN, 11-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
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 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 fveq1 ⊢ f = F → f ⁡ k + f y ∈ I ⟼ if y = X 1 0 = F ⁡ k + f y ∈ I ⟼ if y = X 1 0
7 6 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
8 7 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
9 reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer
10 9 1 2 elbasov ⊢ F ∈ B → I ∈ V ∧ R ∈ V
11 5 10 syl ⊢ φ → I ∈ V ∧ R ∈ V
12 11 simpld ⊢ φ → I ∈ V
13 11 simprd ⊢ φ → R ∈ V
14 1 2 3 12 13 4 psdfval ⊢ φ → I mPSDer R ⁡ X = f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0
15 ovex ⊢ ℕ 0 I ∈ V
16 3 15 rabex2 ⊢ D ∈ V
17 16 mptex ⊢ k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ V
18 17 a1i ⊢ φ → k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ V
19 8 14 5 18 fvmptd4 ⊢ φ → I mPSDer R ⁡ X ⁡ F = k ∈ D ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0