Metamath Proof Explorer

Theorem psdfval

Description: Give a map between power series and their partial derivatives with respect to a given variable X . (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
Assertion psdfval ⊢ φ → I mPSDer R ⁡ X = f ∈ B ⟼ 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 1 2 3 4 5 psdffval ⊢ φ → I mPSDer R = x ∈ I ⟼ f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0
8 fveq2 ⊢ x = X → k ⁡ x = k ⁡ X
9 8 oveq1d ⊢ x = X → k ⁡ x + 1 = k ⁡ X + 1
10 eqeq2 ⊢ x = X → y = x ↔ y = X
11 10 ifbid ⊢ x = X → if y = x 1 0 = if y = X 1 0
12 11 mpteq2dv ⊢ x = X → y ∈ I ⟼ if y = x 1 0 = y ∈ I ⟼ if y = X 1 0
13 12 oveq2d ⊢ x = X → k + f y ∈ I ⟼ if y = x 1 0 = k + f y ∈ I ⟼ if y = X 1 0
14 13 fveq2d ⊢ x = X → f ⁡ k + f y ∈ I ⟼ if y = x 1 0 = f ⁡ k + f y ∈ I ⟼ if y = X 1 0
15 9 14 oveq12d ⊢ x = X → 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
16 15 mpteq2dv ⊢ x = X → 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
17 16 mpteq2dv ⊢ x = X → f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0 = f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0
18 17 adantl ⊢ φ ∧ x = X → f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0 = f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0
19 2 fvexi ⊢ B ∈ V
20 19 a1i ⊢ φ → B ∈ V
21 20 mptexd ⊢ φ → f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ V
22 7 18 6 21 fvmptd ⊢ φ → I mPSDer R ⁡ X = f ∈ B ⟼ k ∈ D ⟼ k ⁡ X + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = X 1 0