Metamath Proof Explorer

Theorem psdffval

Description: Value of the power series differentiation operation. (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
Assertion psdffval ⊢ φ → I mPSDer R = x ∈ I ⟼ 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 df-psd ⊢ mPSDer = i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ Base i mPwSer r ⟼ k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ k ⁡ x + 1 ⋅ r f ⁡ k + f y ∈ i ⟼ if y = x 1 0
7 6 a1i ⊢ φ → mPSDer = i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ Base i mPwSer r ⟼ k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ k ⁡ x + 1 ⋅ r f ⁡ k + f y ∈ i ⟼ if y = x 1 0
8 simpl ⊢ i = I ∧ r = R → i = I
9 oveq12 ⊢ i = I ∧ r = R → i mPwSer r = I mPwSer R
10 9 1 eqtr4di ⊢ i = I ∧ r = R → i mPwSer r = S
11 10 fveq2d ⊢ i = I ∧ r = R → Base i mPwSer r = Base S
12 11 2 eqtr4di ⊢ i = I ∧ r = R → Base i mPwSer r = B
13 8 oveq2d ⊢ i = I ∧ r = R → ℕ 0 i = ℕ 0 I
14 13 rabeqdv ⊢ i = I ∧ r = R → h ∈ ℕ 0 i | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
15 14 3 eqtr4di ⊢ i = I ∧ r = R → h ∈ ℕ 0 i | h -1 ℕ ∈ Fin = D
16 fveq2 ⊢ r = R → ⋅ r = ⋅ R
17 16 adantl ⊢ i = I ∧ r = R → ⋅ r = ⋅ R
18 eqidd ⊢ i = I ∧ r = R → k ⁡ x + 1 = k ⁡ x + 1
19 8 mpteq1d ⊢ i = I ∧ r = R → y ∈ i ⟼ if y = x 1 0 = y ∈ I ⟼ if y = x 1 0
20 19 oveq2d ⊢ i = I ∧ r = R → k + f y ∈ i ⟼ if y = x 1 0 = k + f y ∈ I ⟼ if y = x 1 0
21 20 fveq2d ⊢ i = I ∧ r = R → f ⁡ k + f y ∈ i ⟼ if y = x 1 0 = f ⁡ k + f y ∈ I ⟼ if y = x 1 0
22 17 18 21 oveq123d ⊢ i = I ∧ r = R → 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
23 15 22 mpteq12dv ⊢ i = I ∧ r = R → k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ 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
24 12 23 mpteq12dv ⊢ i = I ∧ r = R → f ∈ Base i mPwSer r ⟼ k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ 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
25 8 24 mpteq12dv ⊢ i = I ∧ r = R → x ∈ i ⟼ f ∈ Base i mPwSer r ⟼ k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ k ⁡ x + 1 ⋅ r f ⁡ k + f y ∈ i ⟼ if y = x 1 0 = x ∈ I ⟼ f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0
26 25 adantl ⊢ φ ∧ i = I ∧ r = R → x ∈ i ⟼ f ∈ Base i mPwSer r ⟼ k ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ k ⁡ x + 1 ⋅ r f ⁡ k + f y ∈ i ⟼ if y = x 1 0 = x ∈ I ⟼ f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0
27 4 elexd ⊢ φ → I ∈ V
28 5 elexd ⊢ φ → R ∈ V
29 4 mptexd ⊢ φ → x ∈ I ⟼ f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0 ∈ V
30 7 26 27 28 29 ovmpod ⊢ φ → I mPSDer R = x ∈ I ⟼ f ∈ B ⟼ k ∈ D ⟼ k ⁡ x + 1 ⋅ R f ⁡ k + f y ∈ I ⟼ if y = x 1 0