evlsmhpvvval

Description: Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval is that b e. D is restricted to b e. G , that is, we can evaluate an N -th degree homogeneous polynomial over just the terms where the sum of all variable degrees is N . (Contributed by SN, 5-Mar-2025)

	Ref	Expression
Hypotheses	evlsmhpvvval.q	\|- Q = ( ( I evalSub S ) ` R )
	evlsmhpvvval.p	\|- H = ( I mHomP U )
	evlsmhpvvval.u	\|- U = ( S \|`s R )
	evlsmhpvvval.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
	evlsmhpvvval.g	\|- G = { g e. D \| ( ( CCfld \|`s NN0 ) gsum g ) = N }
	evlsmhpvvval.k	\|- K = ( Base ` S )
	evlsmhpvvval.m	\|- M = ( mulGrp ` S )
	evlsmhpvvval.w	\|- .^ = ( .g ` M )
	evlsmhpvvval.x	\|- .x. = ( .r ` S )
	evlsmhpvvval.s	\|- ( ph -> S e. CRing )
	evlsmhpvvval.r	\|- ( ph -> R e. ( SubRing ` S ) )
	evlsmhpvvval.f	\|- ( ph -> F e. ( H ` N ) )
	evlsmhpvvval.a	\|- ( ph -> A e. ( K ^m I ) )
Assertion	evlsmhpvvval	\|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. G \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsmhpvvval.q	\|- Q = ( ( I evalSub S ) ` R )
2		evlsmhpvvval.p	\|- H = ( I mHomP U )
3		evlsmhpvvval.u	\|- U = ( S \|`s R )
4		evlsmhpvvval.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
5		evlsmhpvvval.g	\|- G = { g e. D \| ( ( CCfld \|`s NN0 ) gsum g ) = N }
6		evlsmhpvvval.k	\|- K = ( Base ` S )
7		evlsmhpvvval.m	\|- M = ( mulGrp ` S )
8		evlsmhpvvval.w	\|- .^ = ( .g ` M )
9		evlsmhpvvval.x	\|- .x. = ( .r ` S )
10		evlsmhpvvval.s	\|- ( ph -> S e. CRing )
11		evlsmhpvvval.r	\|- ( ph -> R e. ( SubRing ` S ) )
12		evlsmhpvvval.f	\|- ( ph -> F e. ( H ` N ) )
13		evlsmhpvvval.a	\|- ( ph -> A e. ( K ^m I ) )
14		eqid	\|- ( I mPoly U ) = ( I mPoly U )
15		eqid	\|- ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) )
16		reldmmhp	\|- Rel dom mHomP
17	16 2 12	elfvov1	\|- ( ph -> I e. _V )
18	2 14 15 12	mhpmpl	\|- ( ph -> F e. ( Base ` ( I mPoly U ) ) )
19	1 14 15 3 4 6 7 8 9 17 10 11 18 13	evlsvvval	\|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
20		eqid	\|- ( 0g ` S ) = ( 0g ` S )
21	10	crngringd	\|- ( ph -> S e. Ring )
22	21	ringcmnd	\|- ( ph -> S e. CMnd )
23		ovex	\|- ( NN0 ^m I ) e. _V
24	4 23	rabex2	\|- D e. _V
25	24	a1i	\|- ( ph -> D e. _V )
26	21	adantr	\|- ( ( ph /\ b e. D ) -> S e. Ring )
27		eqid	\|- ( Base ` U ) = ( Base ` U )
28	14 27 15 4 18	mplelf	\|- ( ph -> F : D --> ( Base ` U ) )
29	3	subrgbas	\|- ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
30	6	subrgss	\|- ( R e. ( SubRing ` S ) -> R C_ K )
31	29 30	eqsstrrd	\|- ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K )
32	11 31	syl	\|- ( ph -> ( Base ` U ) C_ K )
33	28 32	fssd	\|- ( ph -> F : D --> K )
34	33	ffvelcdmda	\|- ( ( ph /\ b e. D ) -> ( F ` b ) e. K )
35	17	adantr	\|- ( ( ph /\ b e. D ) -> I e. _V )
36	10	adantr	\|- ( ( ph /\ b e. D ) -> S e. CRing )
37	13	adantr	\|- ( ( ph /\ b e. D ) -> A e. ( K ^m I ) )
38		simpr	\|- ( ( ph /\ b e. D ) -> b e. D )
39	4 6 7 8 35 36 37 38	evlsvvvallem	\|- ( ( ph /\ b e. D ) -> ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K )
40	6 9 26 34 39	ringcld	\|- ( ( ph /\ b e. D ) -> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) e. K )
41	40	fmpttd	\|- ( ph -> ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) : D --> K )
42	3 20	subrg0	\|- ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
43	11 42	syl	\|- ( ph -> ( 0g ` S ) = ( 0g ` U ) )
44	43	oveq2d	\|- ( ph -> ( F supp ( 0g ` S ) ) = ( F supp ( 0g ` U ) ) )
45		eqid	\|- ( 0g ` U ) = ( 0g ` U )
46	2 45 4 12	mhpdeg	\|- ( ph -> ( F supp ( 0g ` U ) ) C_ { g e. D \| ( ( CCfld \|`s NN0 ) gsum g ) = N } )
47	46 5	sseqtrrdi	\|- ( ph -> ( F supp ( 0g ` U ) ) C_ G )
48	44 47	eqsstrd	\|- ( ph -> ( F supp ( 0g ` S ) ) C_ G )
49		fvexd	\|- ( ph -> ( 0g ` S ) e. _V )
50	33 48 25 49	suppssr	\|- ( ( ph /\ b e. ( D \ G ) ) -> ( F ` b ) = ( 0g ` S ) )
51	50	oveq1d	\|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) )
52	21	adantr	\|- ( ( ph /\ b e. ( D \ G ) ) -> S e. Ring )
53		eldifi	\|- ( b e. ( D \ G ) -> b e. D )
54	53 39	sylan2	\|- ( ( ph /\ b e. ( D \ G ) ) -> ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K )
55	6 9 20 52 54	ringlzd	\|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( 0g ` S ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) )
56	51 55	eqtrd	\|- ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) )
57	56 25	suppss2	\|- ( ph -> ( ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) supp ( 0g ` S ) ) C_ G )
58	4 14 3 15 6 7 8 9 17 10 11 18 13	evlsvvvallem2	\|- ( ph -> ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) finSupp ( 0g ` S ) )
59	6 20 22 25 41 57 58	gsumres	\|- ( ph -> ( S gsum ( ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) \|` G ) ) = ( S gsum ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
60	5	ssrab3	\|- G C_ D
61	60	a1i	\|- ( ph -> G C_ D )
62	61	resmptd	\|- ( ph -> ( ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) \|` G ) = ( b e. G \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) )
63	62	oveq2d	\|- ( ph -> ( S gsum ( ( b e. D \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) \|` G ) ) = ( S gsum ( b e. G \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
64	19 59 63	3eqtr2d	\|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. G \|-> ( ( F ` b ) .x. ( M gsum ( i e. I \|-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem evlsmhpvvval

Proof