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=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsmhpvvval.p	$$⊢H=I\mathrm{mHomP}U$$
	evlsmhpvvval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsmhpvvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsmhpvvval.g	$$⊢G=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
	evlsmhpvvval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsmhpvvval.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evlsmhpvvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsmhpvvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlsmhpvvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsmhpvvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsmhpvvval.f	$$⊢\phi \to F\in H\left(N\right)$$
	evlsmhpvvval.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	evlsmhpvvval	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{b\in G}{{\sum }_S}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlsmhpvvval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsmhpvvval.p	$$⊢H=I\mathrm{mHomP}U$$
3		evlsmhpvvval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evlsmhpvvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		evlsmhpvvval.g	$$⊢G=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
6		evlsmhpvvval.k	$$⊢K={\mathrm{Base}}_S$$
7		evlsmhpvvval.m	$$⊢M={\mathrm{mulGrp}}_S$$
8		evlsmhpvvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
9		evlsmhpvvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
10		evlsmhpvvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
11		evlsmhpvvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
12		evlsmhpvvval.f	$$⊢\phi \to F\in H\left(N\right)$$
13		evlsmhpvvval.a	$$⊢\phi \to A\in \left(K^I\right)$$
14		eqid	$$⊢I\mathrm{mPoly}U=I\mathrm{mPoly}U$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
16		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
17	16 2 12	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
18	2 14 15 12	mhpmpl	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
19	1 14 15 3 4 6 7 8 9 17 10 11 18 13	evlsvvval	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{b\in D}{{\sum }_S}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
20		eqid	$$⊢0_S=0_S$$
21	10	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
22	21	ringcmnd	$$⊢\phi \to S\in \mathrm{CMnd}$$
23		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
24	4 23	rabex2	$$⊢D\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to D\in \mathrm{V}$$
26	21	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{Ring}$$
27		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
28	14 27 15 4 18	mplelf	$$⊢\phi \to F:D⟶{\mathrm{Base}}_U$$
29	3	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
30	6	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
31	29 30	eqsstrrd	$$⊢R\in \mathrm{SubRing}\left(S\right)\to {\mathrm{Base}}_U\subseteq K$$
32	11 31	syl	$$⊢\phi \to {\mathrm{Base}}_U\subseteq K$$
33	28 32	fssd	$$⊢\phi \to F:D⟶K$$
34	33	ffvelcdmda	$$⊢\left(\phi \wedge b\in D\right)\to F\left(b\right)\in K$$
35	17	adantr	$$⊢\left(\phi \wedge b\in D\right)\to I\in \mathrm{V}$$
36	10	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{CRing}$$
37	13	adantr	$$⊢\left(\phi \wedge b\in D\right)\to A\in \left(K^I\right)$$
38		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
39	4 6 7 8 35 36 37 38	evlsvvvallem	$$⊢\left(\phi \wedge b\in D\right)\to \underset{i\in I}{{\sum }_M}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in K$$
40	6 9 26 34 39	ringcld	$$⊢\left(\phi \wedge b\in D\right)\to F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\in K$$
41	40	fmpttd	$$⊢\phi \to \left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right):D⟶K$$
42	3 20	subrg0	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 0_S=0_U$$
43	11 42	syl	$$⊢\phi \to 0_S=0_U$$
44	43	oveq2d	$$⊢\phi \to F\mathrm{supp}{0}_S=F\mathrm{supp}{0}_U$$
45		eqid	$$⊢0_U=0_U$$
46	2 45 4 12	mhpdeg	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
47	46 5	sseqtrrdi	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq G$$
48	44 47	eqsstrd	$$⊢\phi \to F\mathrm{supp}{0}_S\subseteq G$$
49		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
50	33 48 25 49	suppssr	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to F\left(b\right)=0_S$$
51	50	oveq1d	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)=0_S\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)$$
52	21	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to S\in \mathrm{Ring}$$
53		eldifi	$$⊢b\in \left(D\setminus G\right)\to b\in D$$
54	53 39	sylan2	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to \underset{i\in I}{{\sum }_M}\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\in K$$
55	6 9 20 52 54	ringlzd	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to 0_S\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)=0_S$$
56	51 55	eqtrd	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)=0_S$$
57	56 25	suppss2	$$⊢\phi \to \left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\mathrm{supp}{0}_S\subseteq G$$
58	4 14 3 15 6 7 8 9 17 10 11 18 13	evlsvvvallem2	$$⊢\phi \to {finSupp}_{0_S}\left(\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\right)$$
59	6 20 22 25 41 57 58	gsumres	$$⊢\phi \to {\sum }_S\left({\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\upharpoonright }_G\right)=\underset{b\in D}{{\sum }_S}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
60	5	ssrab3	$$⊢G\subseteq D$$
61	60	a1i	$$⊢\phi \to G\subseteq D$$
62	61	resmptd	$$⊢\phi \to {\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\upharpoonright }_G=\left(b\in G⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
63	62	oveq2d	$$⊢\phi \to {\sum }_S\left({\left(b\in D⟼F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)\upharpoonright }_G\right)=\underset{b\in G}{{\sum }_S}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
64	19 59 63	3eqtr2d	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{b\in G}{{\sum }_S}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$