evlvvvallem

Description: Lemma for theorems using evlvvval . Version of evlsvvvallem2 using df-evl . (Contributed by SN, 11-Mar-2025)

	Ref	Expression
Hypotheses	evlvvvallem.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
	evlvvvallem.p	\|- P = ( I mPoly R )
	evlvvvallem.b	\|- B = ( Base ` P )
	evlvvvallem.k	\|- K = ( Base ` R )
	evlvvvallem.m	\|- M = ( mulGrp ` R )
	evlvvvallem.w	\|- .^ = ( .g ` M )
	evlvvvallem.x	\|- .x. = ( .r ` R )
	evlvvvallem.i	\|- ( ph -> I e. V )
	evlvvvallem.r	\|- ( ph -> R e. CRing )
	evlvvvallem.f	\|- ( ph -> F e. B )
	evlvvvallem.a	\|- ( ph -> A e. ( K ^m I ) )
Assertion	evlvvvallem	\|- ( ph -> ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` R ) )

Step	Hyp	Ref	Expression
1		evlvvvallem.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
2		evlvvvallem.p	\|- P = ( I mPoly R )
3		evlvvvallem.b	\|- B = ( Base ` P )
4		evlvvvallem.k	\|- K = ( Base ` R )
5		evlvvvallem.m	\|- M = ( mulGrp ` R )
6		evlvvvallem.w	\|- .^ = ( .g ` M )
7		evlvvvallem.x	\|- .x. = ( .r ` R )
8		evlvvvallem.i	\|- ( ph -> I e. V )
9		evlvvvallem.r	\|- ( ph -> R e. CRing )
10		evlvvvallem.f	\|- ( ph -> F e. B )
11		evlvvvallem.a	\|- ( ph -> A e. ( K ^m I ) )
12		eqid	\|- ( I mPoly ( R \|`s K ) ) = ( I mPoly ( R \|`s K ) )
13		eqid	\|- ( R \|`s K ) = ( R \|`s K )
14		eqid	\|- ( Base ` ( I mPoly ( R \|`s K ) ) ) = ( Base ` ( I mPoly ( R \|`s K ) ) )
15	9	crngringd	\|- ( ph -> R e. Ring )
16	4	subrgid	\|- ( R e. Ring -> K e. ( SubRing ` R ) )
17	15 16	syl	\|- ( ph -> K e. ( SubRing ` R ) )
18	4	ressid	\|- ( R e. CRing -> ( R \|`s K ) = R )
19	9 18	syl	\|- ( ph -> ( R \|`s K ) = R )
20	19	oveq2d	\|- ( ph -> ( I mPoly ( R \|`s K ) ) = ( I mPoly R ) )
21	20 2	eqtr4di	\|- ( ph -> ( I mPoly ( R \|`s K ) ) = P )
22	21	fveq2d	\|- ( ph -> ( Base ` ( I mPoly ( R \|`s K ) ) ) = ( Base ` P ) )
23	22 3	eqtr4di	\|- ( ph -> ( Base ` ( I mPoly ( R \|`s K ) ) ) = B )
24	10 23	eleqtrrd	\|- ( ph -> F e. ( Base ` ( I mPoly ( R \|`s K ) ) ) )
25	1 12 13 14 4 5 6 7 8 9 17 24 11	evlsvvvallem2	\|- ( ph -> ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` R ) )

Metamath Proof Explorer