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