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 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdcl.b 𝐵 = ( Base ‘ 𝑆 )
psdcl.r ( 𝜑𝑅 ∈ Mgm )
psdcl.x ( 𝜑𝑋𝐼 )
psdcl.f ( 𝜑𝐹𝐵 )
Assertion psdcl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psdcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdcl.b 𝐵 = ( Base ‘ 𝑆 )
3 psdcl.r ( 𝜑𝑅 ∈ Mgm )
4 psdcl.x ( 𝜑𝑋𝐼 )
5 psdcl.f ( 𝜑𝐹𝐵 )
6 fvexd ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
7 ovex ( ℕ0m 𝐼 ) ∈ V
8 7 rabex { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V
9 8 a1i ( 𝜑 → { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V )
10 3 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Mgm )
11 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
12 11 psrbagf ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → 𝑘 : 𝐼 ⟶ ℕ0 )
13 12 adantl ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
14 4 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑋𝐼 )
15 13 14 ffvelcdmd ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘𝑋 ) ∈ ℕ0 )
16 nn0p1nn ( ( 𝑘𝑋 ) ∈ ℕ0 → ( ( 𝑘𝑋 ) + 1 ) ∈ ℕ )
17 15 16 syl ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑘𝑋 ) + 1 ) ∈ ℕ )
18 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 1 18 11 2 5 psrelbas ( 𝜑𝐹 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20 19 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝐹 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
21 simpr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
22 reldmpsr Rel dom mPwSer
23 1 2 22 strov2rcl ( 𝐹𝐵𝐼 ∈ V )
24 5 23 syl ( 𝜑𝐼 ∈ V )
25 1nn0 1 ∈ ℕ0
26 11 snifpsrbag ( ( 𝐼 ∈ V ∧ 1 ∈ ℕ0 ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
27 24 25 26 sylancl ( 𝜑 → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
28 27 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
29 11 psrbagaddcl ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
30 21 28 29 syl2anc ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
31 20 30 ffvelcdmd ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
32 eqid ( .g𝑅 ) = ( .g𝑅 )
33 18 32 mulgnncl ( ( 𝑅 ∈ Mgm ∧ ( ( 𝑘𝑋 ) + 1 ) ∈ ℕ ∧ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
34 10 17 31 33 syl3anc ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
35 34 fmpttd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
36 6 9 35 elmapdd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
37 1 2 11 4 5 psdval ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
38 1 18 11 2 24 psrbas ( 𝜑𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
39 36 37 38 3eltr4d ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )