This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
8 7 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
9 8 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Mgm )
11 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
12 11 psrbagf ⊢ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑘 : 𝐼 ⟶ ℕ0 )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑋 ∈ 𝐼 )
15 13 14 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ‘ 𝑋 ) ∈ ℕ0 )
16 nn0p1nn ⊢ ( ( 𝑘 ‘ 𝑋 ) ∈ ℕ0 → ( ( 𝑘 ‘ 𝑋 ) + 1 ) ∈ ℕ )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑘 ‘ 𝑋 ) + 1 ) ∈ ℕ )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 1 18 11 2 5 psrelbas ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
27 24 25 26 sylancl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
29 11 psrbagaddcl ⊢ ( ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
30 21 28 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
31 20 30 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
35 34 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
36 6 9 35 elmapdd ⊢ ( 𝜑 → ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
37 1 2 11 4 5 psdval ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
38 1 18 11 2 24 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
39 36 37 38 3eltr4d ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )