Metamath Proof Explorer

Theorem psdfval

Description: Give a map between power series and their partial derivatives with respect to a given variable X . (Contributed by SN, 11-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 psdffval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdffval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdffval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
4 psdffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psdffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
6 psdfval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7 1 2 3 4 5 psdffval ⊢ ( 𝜑 → ( 𝐼 mPSDer 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )
8 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ‘ 𝑥 ) = ( 𝑘 ‘ 𝑋 ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑘 ‘ 𝑥 ) + 1 ) = ( ( 𝑘 ‘ 𝑋 ) + 1 ) )
10 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 = 𝑥 ↔ 𝑦 = 𝑋 ) )
11 10 ifbid ⊢ ( 𝑥 = 𝑋 → if ( 𝑦 = 𝑥 , 1 , 0 ) = if ( 𝑦 = 𝑋 , 1 , 0 ) )
12 11 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
13 12 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) = ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
14 13 fveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) = ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
15 9 14 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
16 15 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
17 16 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
19 2 fvexi ⊢ 𝐵 ∈ V
20 19 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
21 20 mptexd ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) ∈ V )
22 7 18 6 21 fvmptd ⊢ ( 𝜑 → ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )