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 
|- 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 )
Assertion 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 ) ) ) ) ) ) ) )

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 1 2 3 4 5 psdffval 
 |-  ( ph -> ( I mPSDer R ) = ( x e. I |-> ( f e. B |-> ( k e. D |-> ( ( ( k ` x ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )
8 fveq2 
 |-  ( x = X -> ( k ` x ) = ( k ` X ) )
9 8 oveq1d 
 |-  ( x = X -> ( ( k ` x ) + 1 ) = ( ( k ` X ) + 1 ) )
10 eqeq2 
 |-  ( x = X -> ( y = x <-> y = X ) )
11 10 ifbid 
 |-  ( x = X -> if ( y = x , 1 , 0 ) = if ( y = X , 1 , 0 ) )
12 11 mpteq2dv 
 |-  ( x = X -> ( y e. I |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) )
13 12 oveq2d 
 |-  ( x = X -> ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) = ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
14 13 fveq2d 
 |-  ( x = X -> ( f ` ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) = ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
15 9 14 oveq12d 
 |-  ( x = X -> ( ( ( 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 ) ) ) ) ) )
16 15 mpteq2dv 
 |-  ( x = X -> ( 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 ) ) ) ) ) ) )
17 16 mpteq2dv 
 |-  ( x = X -> ( f e. B |-> ( k e. D |-> ( ( ( k ` x ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) = ( f e. B |-> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) )
18 17 adantl 
 |-  ( ( ph /\ x = X ) -> ( f e. B |-> ( k e. D |-> ( ( ( k ` x ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) = ( f e. B |-> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) )
19 2 fvexi 
 |-  B e. _V
20 19 a1i 
 |-  ( ph -> B e. _V )
21 20 mptexd 
 |-  ( ph -> ( f e. B |-> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) e. _V )
22 7 18 6 21 fvmptd 
 |-  ( 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 ) ) ) ) ) ) ) )