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