Metamath Proof Explorer

Theorem psdffval

Description: Value of the power series differentiation operation. (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 )
Assertion 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 ) ) ) ) ) ) ) ) )

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 df-psd 
 |-  mPSDer = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) )
7 6 a1i 
 |-  ( ph -> mPSDer = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) ) )
8 simpl 
 |-  ( ( i = I /\ r = R ) -> i = I )
9 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPwSer r ) = ( I mPwSer R ) )
10 9 1 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( i mPwSer r ) = S )
11 10 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPwSer r ) ) = ( Base ` S ) )
12 11 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPwSer r ) ) = B )
13 8 oveq2d 
 |-  ( ( i = I /\ r = R ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
14 13 rabeqdv 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
15 14 3 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
16 fveq2 
 |-  ( r = R -> ( .g ` r ) = ( .g ` R ) )
17 16 adantl 
 |-  ( ( i = I /\ r = R ) -> ( .g ` r ) = ( .g ` R ) )
18 eqidd 
 |-  ( ( i = I /\ r = R ) -> ( ( k ` x ) + 1 ) = ( ( k ` x ) + 1 ) )
19 8 mpteq1d 
 |-  ( ( i = I /\ r = R ) -> ( y e. i |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = x , 1 , 0 ) ) )
20 19 oveq2d 
 |-  ( ( i = I /\ r = R ) -> ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) = ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) )
21 20 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) = ( f ` ( k oF + ( y e. I |-> if ( y = x , 1 , 0 ) ) ) ) )
22 17 18 21 oveq123d 
 |-  ( ( i = I /\ r = R ) -> ( ( ( 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 ) ) ) ) ) )
23 15 22 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( 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 ) ) ) ) ) ) )
24 12 23 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( 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 ) ) ) ) ) ) ) )
25 8 24 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) ) )
26 25 adantl 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> ( x e. i |-> ( f e. ( Base ` ( i mPwSer r ) ) |-> ( k e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` x ) + 1 ) ( .g ` r ) ( f ` ( k oF + ( y e. i |-> if ( y = x , 1 , 0 ) ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) ) )
27 4 elexd 
 |-  ( ph -> I e. _V )
28 5 elexd 
 |-  ( ph -> R e. _V )
29 4 mptexd 
 |-  ( ph -> ( 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 ) ) ) ) ) ) ) ) e. _V )
30 7 26 27 28 29 ovmpod 
 |-  ( 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 ) ) ) ) ) ) ) ) )