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.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.r ⊢ φ → R ∈ Mgm
4 psdcl.x ⊢ φ → X ∈ I
5 psdcl.f ⊢ φ → F ∈ B
6 fvexd ⊢ φ → Base R ∈ V
7 ovex ⊢ ℕ 0 I ∈ V
8 7 rabex ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
9 8 a1i ⊢ φ → h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
10 3 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Mgm
11 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
12 11 psrbagf ⊢ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
13 12 adantl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k : I ⟶ ℕ 0
14 4 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
15 13 14 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X ∈ ℕ 0
16 nn0p1nn ⊢ k ⁡ X ∈ ℕ 0 → k ⁡ X + 1 ∈ ℕ
17 15 16 syl ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ∈ ℕ
18 eqid ⊢ Base R = Base R
19 1 18 11 2 5 psrelbas ⊢ φ → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
20 19 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
21 simpr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
22 reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer
23 1 2 22 strov2rcl ⊢ F ∈ B → I ∈ V
24 5 23 syl ⊢ φ → I ∈ V
25 1nn0 ⊢ 1 ∈ ℕ 0
26 11 snifpsrbag ⊢ I ∈ V ∧ 1 ∈ ℕ 0 → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
27 24 25 26 sylancl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
28 27 adantr ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
29 11 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
30 21 28 29 syl2anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
31 20 30 ffvelcdmd ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
32 eqid ⊢ ⋅ R = ⋅ R
33 18 32 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
34 10 17 31 33 syl3anc ⊢ φ ∧ k ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → k ⁡ X + 1 ⋅ R F ⁡ k + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
35 34 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
36 6 9 35 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
37 1 2 11 4 5 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
38 1 18 11 2 24 psrbas ⊢ φ → B = Base R h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
39 36 37 38 3eltr4d ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B