Metamath Proof Explorer

Theorem psdvsca

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

Ref Expression
Hypotheses psdvsca.s ⊢ S = I mPwSer R
psdvsca.b ⊢ B = Base S
psdvsca.m ⊢ · ˙ = ⋅ S
psdvsca.k ⊢ K = Base R
psdvsca.i ⊢ φ → I ∈ V
psdvsca.r ⊢ φ → R ∈ CRing
psdvsca.x ⊢ φ → X ∈ I
psdvsca.f ⊢ φ → F ∈ B
psdvsca.c ⊢ φ → C ∈ K
Assertion psdvsca ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F = C · ˙ I mPSDer R ⁡ X ⁡ F

Proof

Step Hyp Ref Expression
1 psdvsca.s ⊢ S = I mPwSer R
2 psdvsca.b ⊢ B = Base S
3 psdvsca.m ⊢ · ˙ = ⋅ S
4 psdvsca.k ⊢ K = Base R
5 psdvsca.i ⊢ φ → I ∈ V
6 psdvsca.r ⊢ φ → R ∈ CRing
7 psdvsca.x ⊢ φ → X ∈ I
8 psdvsca.f ⊢ φ → F ∈ B
9 psdvsca.c ⊢ φ → C ∈ K
10 eqid ⊢ Base R = Base R
11 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
12 6 crngringd ⊢ φ → R ∈ Ring
13 ringmgm ⊢ R ∈ Ring → R ∈ Mgm
14 12 13 syl ⊢ φ → R ∈ Mgm
15 1 3 4 2 12 9 8 psrvscacl ⊢ φ → C · ˙ F ∈ B
16 1 2 5 14 7 15 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F ∈ B
17 1 10 11 2 16 psrelbas ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
18 17 ffnd ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
19 1 2 5 14 7 8 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B
20 1 3 4 2 12 9 19 psrvscacl ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F ∈ B
21 1 10 11 2 20 psrelbas ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
22 21 ffnd ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
23 12 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Ring
24 11 psrbagf ⊢ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
25 24 adantl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
26 7 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
27 25 26 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X ∈ ℕ 0
28 peano2nn0 ⊢ d ⁡ X ∈ ℕ 0 → d ⁡ X + 1 ∈ ℕ 0
29 28 nn0zd ⊢ d ⁡ X ∈ ℕ 0 → d ⁡ X + 1 ∈ ℤ
30 27 29 syl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ∈ ℤ
31 9 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C ∈ K
32 1 4 11 2 8 psrelbas ⊢ φ → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ K
33 32 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ K
34 simpr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
35 11 psrbagsn ⊢ I ∈ V → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
36 5 35 syl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
37 36 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
38 11 psrbagaddcl ⊢ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
39 34 37 38 syl2anc ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
40 33 39 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ K
41 eqid ⊢ ⋅ R = ⋅ R
42 eqid ⊢ ⋅ R = ⋅ R
43 4 41 42 mulgass3 ⊢ R ∈ Ring ∧ d ⁡ X + 1 ∈ ℤ ∧ C ∈ K ∧ F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ K → C ⋅ R d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R C ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
44 23 30 31 40 43 syl13anc ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C ⋅ R d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R C ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
45 5 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I ∈ V
46 6 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ CRing
47 8 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ∈ B
48 1 2 11 45 46 26 47 34 psdcoef ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I mPSDer R ⁡ X ⁡ F ⁡ d = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
49 48 oveq2d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C ⋅ R I mPSDer R ⁡ X ⁡ F ⁡ d = C ⋅ R d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
50 1 3 4 2 42 11 31 47 39 psrvscaval ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C · ˙ F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = C ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
51 50 oveq2d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R C · ˙ F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R C ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
52 44 49 51 3eqtr4rd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R C · ˙ F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = C ⋅ R I mPSDer R ⁡ X ⁡ F ⁡ d
53 15 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C · ˙ F ∈ B
54 1 2 11 45 46 26 53 34 psdcoef ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I mPSDer R ⁡ X ⁡ C · ˙ F ⁡ d = d ⁡ X + 1 ⋅ R C · ˙ F ⁡ d + f y ∈ I ⟼ if y = X 1 0
55 19 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I mPSDer R ⁡ X ⁡ F ∈ B
56 1 3 4 2 42 11 31 55 34 psrvscaval ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C · ˙ I mPSDer R ⁡ X ⁡ F ⁡ d = C ⋅ R I mPSDer R ⁡ X ⁡ F ⁡ d
57 52 54 56 3eqtr4d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I mPSDer R ⁡ X ⁡ C · ˙ F ⁡ d = C · ˙ I mPSDer R ⁡ X ⁡ F ⁡ d
58 18 22 57 eqfnfvd ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F = C · ˙ I mPSDer R ⁡ X ⁡ F