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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 ) ) ) ) ) ) ) )