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.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.r ⊢ φ → R ∈ CRing
6 psdvsca.x ⊢ φ → X ∈ I
7 psdvsca.f ⊢ φ → F ∈ B
8 psdvsca.c ⊢ φ → C ∈ K
9 eqid ⊢ Base R = Base R
10 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
11 5 crngringd ⊢ φ → R ∈ Ring
12 ringmgm ⊢ R ∈ Ring → R ∈ Mgm
13 11 12 syl ⊢ φ → R ∈ Mgm
14 1 3 4 2 11 8 7 psrvscacl ⊢ φ → C · ˙ F ∈ B
15 1 2 13 6 14 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F ∈ B
16 1 9 10 2 15 psrelbas ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
17 16 ffnd ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
18 1 2 13 6 7 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B
19 1 3 4 2 11 8 18 psrvscacl ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F ∈ B
20 1 9 10 2 19 psrelbas ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
21 20 ffnd ⊢ φ → C · ˙ I mPSDer R ⁡ X ⁡ F Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
22 11 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ Ring
23 10 psrbagf ⊢ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
24 23 adantl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
25 6 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
26 24 25 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X ∈ ℕ 0
27 peano2nn0 ⊢ d ⁡ X ∈ ℕ 0 → d ⁡ X + 1 ∈ ℕ 0
28 27 nn0zd ⊢ d ⁡ X ∈ ℕ 0 → d ⁡ X + 1 ∈ ℤ
29 26 28 syl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ∈ ℤ
30 8 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C ∈ K
31 1 4 10 2 7 psrelbas ⊢ φ → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ K
32 31 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ K
33 simpr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
34 reldmpsr ⊢ Rel ⁡ dom ⁡ mPwSer
35 1 2 34 strov2rcl ⊢ F ∈ B → I ∈ V
36 7 35 syl ⊢ φ → I ∈ V
37 10 psrbagsn ⊢ I ∈ V → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
38 36 37 syl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
39 38 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
40 10 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
41 33 39 40 syl2anc ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
42 32 41 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ K
43 eqid ⊢ ⋅ R = ⋅ R
44 eqid ⊢ ⋅ R = ⋅ R
45 4 43 44 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
46 22 29 30 42 45 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
47 7 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ∈ B
48 1 2 10 25 47 33 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 44 10 30 47 41 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 46 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 14 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → C · ˙ F ∈ B
54 1 2 10 25 53 33 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 18 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → I mPSDer R ⁡ X ⁡ F ∈ B
56 1 3 4 2 44 10 30 55 33 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 17 21 57 eqfnfvd ⊢ φ → I mPSDer R ⁡ X ⁡ C · ˙ F = C · ˙ I mPSDer R ⁡ X ⁡ F