psdcoef

Description: Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-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 )
	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 ) ) ) ) ) )

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		psdval.f	\|- ( ph -> F e. B )
8		psdcoef.k	\|- ( ph -> K e. D )
9	1 2 3 4 5 6 7	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 ) ) ) ) ) ) )
10		fveq1	\|- ( k = K -> ( k ` X ) = ( K ` X ) )
11	10	oveq1d	\|- ( k = K -> ( ( k ` X ) + 1 ) = ( ( K ` X ) + 1 ) )
12		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 ) ) ) ) )
13	11 12	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 ) ) ) ) ) )
14	13	adantl	\|- ( ( ph /\ 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 ) ) ) ) ) )
15		ovexd	\|- ( ph -> ( ( ( K ` X ) + 1 ) ( .g ` R ) ( F ` ( K oF + ( y e. I \|-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V )
16	9 14 8 15	fvmptd	\|- ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` K ) = ( ( ( K ` X ) + 1 ) ( .g ` R ) ( F ` ( K oF + ( y e. I \|-> if ( y = X , 1 , 0 ) ) ) ) ) )

Metamath Proof Explorer