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