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

Metamath Proof Explorer

Theorem evlsvval

Proof