Metamath Proof Explorer

Theorem psdval

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

Ref Expression
Hypotheses psdval.s 
|- S = ( I mPwSer R )
psdval.b 
|- B = ( Base ` S )
psdval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psdval.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 psdval.s 
 |-  S = ( I mPwSer R )
2 psdval.b 
 |-  B = ( Base ` S )
3 psdval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
4 psdval.x 
 |-  ( ph -> X e. I )
5 psdval.f 
 |-  ( ph -> F e. B )
6 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 ) ) ) ) )
7 6 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 ) ) ) ) ) )
8 7 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 ) ) ) ) ) ) )
9 reldmpsr 
 |-  Rel dom mPwSer
10 9 1 2 elbasov 
 |-  ( F e. B -> ( I e. _V /\ R e. _V ) )
11 5 10 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
12 11 simpld 
 |-  ( ph -> I e. _V )
13 11 simprd 
 |-  ( ph -> R e. _V )
14 1 2 3 12 13 4 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 ) ) ) ) ) ) ) )
15 ovex 
 |-  ( NN0 ^m I ) e. _V
16 3 15 rabex2 
 |-  D e. _V
17 16 mptex 
 |-  ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V
18 17 a1i 
 |-  ( ph -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V )
19 8 14 5 18 fvmptd4 
 |-  ( 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 ) ) ) ) ) ) )