This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psdcoef

Description: Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-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 )
psdcoef.k 
|- ( ph -> K e. D )
Assertion psdcoef 
|- ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` K ) = ( ( ( 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 psdcoef.k 
 |-  ( ph -> K e. D )
7 fveq1 
 |-  ( k = K -> ( k ` X ) = ( K ` X ) )
8 7 oveq1d 
 |-  ( k = K -> ( ( k ` X ) + 1 ) = ( ( K ` X ) + 1 ) )
9 fvoveq1 
 |-  ( k = K -> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( F ` ( K oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
10 8 9 oveq12d 
 |-  ( k = K -> ( ( ( 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 1 2 3 4 5 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 ) ) ) ) ) ) )
12 ovexd 
 |-  ( ph -> ( ( ( K ` X ) + 1 ) ( .g ` R ) ( F ` ( K oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V )
13 10 11 6 12 fvmptd4 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` K ) = ( ( ( K ` X ) + 1 ) ( .g ` R ) ( F ` ( K oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )