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

Metamath Proof Explorer

Theorem psdval

Description: Evaluate the partial derivative of a power series F with respect to X . (Contributed by SN, 11-Apr-2025)

Ref Expression
Hypotheses psdval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psdval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psdval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion psdval ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psdval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
4 psdval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 psdval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
7 6 oveq2d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
8 7 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
9 reldmpsr ⊢ Rel dom mPwSer
10 9 1 2 elbasov ⊢ ( 𝐹 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
11 5 10 syl ⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
12 11 simpld ⊢ ( 𝜑 → 𝐼 ∈ V )
13 11 simprd ⊢ ( 𝜑 → 𝑅 ∈ V )
14 1 2 3 12 13 4 psdfval ⊢ ( 𝜑 → ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
15 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
16 3 15 rabex2 ⊢ 𝐷 ∈ V
17 16 mptex ⊢ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V
18 17 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V )
19 8 14 5 18 fvmptd4 ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )