Metamath Proof Explorer

Theorem psdval

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

Ref Expression
Hypotheses psdffval.s 
|- S = ( I mPwSer R )
psdffval.b 
|- B = ( Base ` S )
psdffval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psdffval.i 
|- ( ph -> I e. V )
psdffval.r 
|- ( ph -> R e. W )
psdfval.x 
|- ( ph -> X e. I )
psdval.f 
|- ( ph -> F e. B )
Assertion psdval 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psdffval.s 
 |-  S = ( I mPwSer R )
2 psdffval.b 
 |-  B = ( Base ` S )
3 psdffval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
4 psdffval.i 
 |-  ( ph -> I e. V )
5 psdffval.r 
 |-  ( ph -> R e. W )
6 psdfval.x 
 |-  ( ph -> X e. I )
7 psdval.f 
 |-  ( ph -> F e. B )
8 1 2 3 4 5 6 psdfval 
 |-  ( ph -> ( ( I mPSDer R ) ` X ) = ( f e. B |-> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) )
9 fveq1 
 |-  ( f = F -> ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
10 9 oveq2d 
 |-  ( f = F -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
11 10 mpteq2dv 
 |-  ( f = F -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
12 11 adantl 
 |-  ( ( ph /\ f = F ) -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 3 13 rabex2 
 |-  D e. _V
15 14 a1i 
 |-  ( ph -> D e. _V )
16 15 mptexd 
 |-  ( ph -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V )
17 8 12 7 16 fvmptd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )