Theorem evlsvval

Description: Give a formula for the evaluation of a polynomial. (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	evlsvval.q	|- Q = ( ( I evalSub S ) ` R )
	evlsvval.p	|- P = ( I mPoly U )
	evlsvval.b	|- B = ( Base ` P )
	evlsvval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	evlsvval.k	|- K = ( Base ` S )
	evlsvval.u	|- U = ( S |`s R )
	evlsvval.t	|- T = ( S ^s ( K ^m I ) )
	evlsvval.m	|- M = ( mulGrp ` T )
	evlsvval.w	|- .^ = ( .g ` M )
	evlsvval.x	|- .x. = ( .r ` T )
	evlsvval.f	|- F = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
	evlsvval.g	|- G = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
	evlsvval.i	|- ( ph -> I e. V )
	evlsvval.s	|- ( ph -> S e. CRing )
	evlsvval.r	|- ( ph -> R e. ( SubRing ` S ) )
	evlsvval.a	|- ( ph -> A e. B )
Assertion	evlsvval	|- ( ph -> ( Q ` A ) = ( T gsum ( b e. D |-> ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvval.q	|- Q = ( ( I evalSub S ) ` R )
2		evlsvval.p	|- P = ( I mPoly U )
3		evlsvval.b	|- B = ( Base ` P )
4		evlsvval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5		evlsvval.k	|- K = ( Base ` S )
6		evlsvval.u	|- U = ( S |`s R )
7		evlsvval.t	|- T = ( S ^s ( K ^m I ) )
8		evlsvval.m	|- M = ( mulGrp ` T )
9		evlsvval.w	|- .^ = ( .g ` M )
10		evlsvval.x	|- .x. = ( .r ` T )
11		evlsvval.f	|- F = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
12		evlsvval.g	|- G = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
13		evlsvval.i	|- ( ph -> I e. V )
14		evlsvval.s	|- ( ph -> S e. CRing )
15		evlsvval.r	|- ( ph -> R e. ( SubRing ` S ) )
16		evlsvval.a	|- ( ph -> A e. B )
17		fveq1	|- ( p = A -> ( p ` b ) = ( A ` b ) )
18	17	fveq2d	|- ( p = A -> ( F ` ( p ` b ) ) = ( F ` ( A ` b ) ) )
19	18	oveq1d	|- ( p = A -> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) = ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) )
20	19	mpteq2dv	|- ( p = A -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) )
21	20	oveq2d	|- ( p = A -> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) = ( T gsum ( b e. D |-> ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )
22		eqid	|- ( p e. B |-> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) ) = ( p e. B |-> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )
23	1 2 3 4 5 6 7 8 9 10 22 11 12 13 14 15	evlsval3	|- ( ph -> Q = ( p e. B |-> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) ) )
24		ovexd	|- ( ph -> ( T gsum ( b e. D |-> ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) e. _V )
25	21 23 16 24	fvmptd4	|- ( ph -> ( Q ` A ) = ( T gsum ( b e. D |-> ( ( F ` ( A ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )