Metamath Proof Explorer

Theorem psdcl

Description: The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025)

Ref Expression
Hypotheses psdcl.s ⊢ S = I mPwSer R
psdcl.b ⊢ B = Base S
psdcl.i ⊢ φ → I ∈ V
psdcl.r ⊢ φ → R ∈ Mgm
psdcl.x ⊢ φ → X ∈ I
psdcl.f ⊢ φ → F ∈ B
Assertion psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B

Proof

Step Hyp Ref Expression
1 psdcl.s ⊢ S = I mPwSer R
2 psdcl.b ⊢ B = Base S
3 psdcl.i ⊢ φ → I ∈ V
4 psdcl.r ⊢ φ → R ∈ Mgm
5 psdcl.x ⊢ φ → X ∈ I
6 psdcl.f ⊢ φ → F ∈ B
7 fvexd ⊢ φ → Base R ∈ V
8 ovex ⊢ ℕ 0 I ∈ V
9 8 rabex ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
10 9 a1i ⊢ φ → h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
11 4 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Mgm
12 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
13 12 psrbagf ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
14 13 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
15 5 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
16 14 15 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X ∈ ℕ 0
17 nn0p1nn ⊢ k ⁡ X ∈ ℕ 0 → k ⁡ X + 1 ∈ ℕ
18 16 17 syl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ∈ ℕ
19 eqid ⊢ Base R = Base R
20 1 19 12 2 6 psrelbas ⊢ φ → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
21 20 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
22 simpr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
23 1nn0 ⊢ 1 ∈ ℕ 0
24 12 snifpsrbag ⊢ I ∈ V ∧ 1 ∈ ℕ 0 → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
25 3 23 24 sylancl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
26 25 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
27 12 psrbagaddcl ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
28 22 26 27 syl2anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
29 21 28 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
30 eqid ⊢ ⋅ R = ⋅ R
31 19 30 mulgnncl ⊢ R ∈ Mgm ∧ k ⁡ X + 1 ∈ ℕ ∧ F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R → k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
32 11 18 29 31 syl3anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
33 32 fmpttd ⊢ φ → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
34 7 10 33 elmapdd ⊢ φ → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
35 1 2 12 3 4 5 6 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ F = k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0
36 1 19 12 2 3 psrbas ⊢ φ → B = Base R h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
37 34 35 36 3eltr4d ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B