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 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdvsca.b 𝐵 = ( Base ‘ 𝑆 )
psdvsca.m · = ( ·𝑠𝑆 )
psdvsca.k 𝐾 = ( Base ‘ 𝑅 )
psdvsca.r ( 𝜑𝑅 ∈ CRing )
psdvsca.x ( 𝜑𝑋𝐼 )
psdvsca.f ( 𝜑𝐹𝐵 )
psdvsca.c ( 𝜑𝐶𝐾 )
Assertion psdvsca ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) = ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 psdvsca.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdvsca.b 𝐵 = ( Base ‘ 𝑆 )
3 psdvsca.m · = ( ·𝑠𝑆 )
4 psdvsca.k 𝐾 = ( Base ‘ 𝑅 )
5 psdvsca.r ( 𝜑𝑅 ∈ CRing )
6 psdvsca.x ( 𝜑𝑋𝐼 )
7 psdvsca.f ( 𝜑𝐹𝐵 )
8 psdvsca.c ( 𝜑𝐶𝐾 )
9 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
11 5 crngringd ( 𝜑𝑅 ∈ Ring )
12 ringmgm ( 𝑅 ∈ Ring → 𝑅 ∈ Mgm )
13 11 12 syl ( 𝜑𝑅 ∈ Mgm )
14 1 3 4 2 11 8 7 psrvscacl ( 𝜑 → ( 𝐶 · 𝐹 ) ∈ 𝐵 )
15 1 2 13 6 14 psdcl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) ∈ 𝐵 )
16 1 9 10 2 15 psrelbas ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
17 16 ffnd ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
18 1 2 13 6 7 psdcl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )
19 1 3 4 2 11 8 18 psrvscacl ( 𝜑 → ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ∈ 𝐵 )
20 1 9 10 2 19 psrelbas ( 𝜑 → ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
21 20 ffnd ( 𝜑 → ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
22 11 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Ring )
23 10 psrbagf ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → 𝑑 : 𝐼 ⟶ ℕ0 )
24 23 adantl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 : 𝐼 ⟶ ℕ0 )
25 6 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑋𝐼 )
26 24 25 ffvelcdmd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑𝑋 ) ∈ ℕ0 )
27 peano2nn0 ( ( 𝑑𝑋 ) ∈ ℕ0 → ( ( 𝑑𝑋 ) + 1 ) ∈ ℕ0 )
28 27 nn0zd ( ( 𝑑𝑋 ) ∈ ℕ0 → ( ( 𝑑𝑋 ) + 1 ) ∈ ℤ )
29 26 28 syl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑑𝑋 ) + 1 ) ∈ ℤ )
30 8 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝐶𝐾 )
31 1 4 10 2 7 psrelbas ( 𝜑𝐹 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ 𝐾 )
32 31 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝐹 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ 𝐾 )
33 simpr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
34 reldmpsr Rel dom mPwSer
35 1 2 34 strov2rcl ( 𝐹𝐵𝐼 ∈ V )
36 7 35 syl ( 𝜑𝐼 ∈ V )
37 10 psrbagsn ( 𝐼 ∈ V → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
38 36 37 syl ( 𝜑 → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
39 38 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
40 10 psrbagaddcl ( ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
41 33 39 40 syl2anc ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
42 32 41 ffvelcdmd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ 𝐾 )
43 eqid ( .g𝑅 ) = ( .g𝑅 )
44 eqid ( .r𝑅 ) = ( .r𝑅 )
45 4 43 44 mulgass3 ( ( 𝑅 ∈ Ring ∧ ( ( ( 𝑑𝑋 ) + 1 ) ∈ ℤ ∧ 𝐶𝐾 ∧ ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ 𝐾 ) ) → ( 𝐶 ( .r𝑅 ) ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐶 ( .r𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
46 22 29 30 42 45 syl13anc ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐶 ( .r𝑅 ) ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐶 ( .r𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
47 7 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝐹𝐵 )
48 1 2 10 25 47 33 psdcoef ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) = ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
49 48 oveq2d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐶 ( .r𝑅 ) ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) ) = ( 𝐶 ( .r𝑅 ) ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
50 1 3 4 2 44 10 30 47 41 psrvscaval ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝐶 · 𝐹 ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐶 ( .r𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
51 50 oveq2d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( ( 𝐶 · 𝐹 ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐶 ( .r𝑅 ) ( 𝐹 ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
52 46 49 51 3eqtr4rd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( ( 𝐶 · 𝐹 ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( 𝐶 ( .r𝑅 ) ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) ) )
53 14 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐶 · 𝐹 ) ∈ 𝐵 )
54 1 2 10 25 53 33 psdcoef ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) ‘ 𝑑 ) = ( ( ( 𝑑𝑋 ) + 1 ) ( .g𝑅 ) ( ( 𝐶 · 𝐹 ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
55 18 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )
56 1 3 4 2 44 10 30 55 33 psrvscaval ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ‘ 𝑑 ) = ( 𝐶 ( .r𝑅 ) ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) ) )
57 52 54 56 3eqtr4d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) ‘ 𝑑 ) = ( ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ‘ 𝑑 ) )
58 17 21 57 eqfnfvd ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 · 𝐹 ) ) = ( 𝐶 · ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) )