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.i	$$⊢\phi \to I\in V$$
	evlsmhpvvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsmhpvvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsmhpvvval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	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.i	$$⊢\phi \to I\in V$$
11		evlsmhpvvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
12		evlsmhpvvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
13		evlsmhpvvval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14		evlsmhpvvval.f	$$⊢\phi \to F\in H\left(N\right)$$
15		evlsmhpvvval.a	$$⊢\phi \to A\in \left(K^I\right)$$
16		eqid	$$⊢I\mathrm{mPoly}U=I\mathrm{mPoly}U$$
17		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
18	3	ovexi	$$⊢U\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to U\in \mathrm{V}$$
20	2 16 17 10 19 13 14	mhpmpl	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}U\right)}$$
21	1 16 17 3 4 6 7 8 9 10 11 12 20 15	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)$$
22		eqid	$$⊢0_S=0_S$$
23	11	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
24	23	ringcmnd	$$⊢\phi \to S\in \mathrm{CMnd}$$
25		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
26	4 25	rabex2	$$⊢D\in \mathrm{V}$$
27	26	a1i	$$⊢\phi \to D\in \mathrm{V}$$
28	23	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{Ring}$$
29		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
30	16 29 17 4 20	mplelf	$$⊢\phi \to F:D⟶{\mathrm{Base}}_U$$
31	3	subrgbas	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R={\mathrm{Base}}_U$$
32	6	subrgss	$$⊢R\in \mathrm{SubRing}\left(S\right)\to R\subseteq K$$
33	31 32	eqsstrrd	$$⊢R\in \mathrm{SubRing}\left(S\right)\to {\mathrm{Base}}_U\subseteq K$$
34	12 33	syl	$$⊢\phi \to {\mathrm{Base}}_U\subseteq K$$
35	30 34	fssd	$$⊢\phi \to F:D⟶K$$
36	35	ffvelcdmda	$$⊢\left(\phi \wedge b\in D\right)\to F\left(b\right)\in K$$
37	10	adantr	$$⊢\left(\phi \wedge b\in D\right)\to I\in V$$
38	11	adantr	$$⊢\left(\phi \wedge b\in D\right)\to S\in \mathrm{CRing}$$
39	15	adantr	$$⊢\left(\phi \wedge b\in D\right)\to A\in \left(K^I\right)$$
40		simpr	$$⊢\left(\phi \wedge b\in D\right)\to b\in D$$
41	4 6 7 8 37 38 39 40	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$$
42	6 9 28 36 41	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$$
43	42	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$$
44	3 22	subrg0	$$⊢R\in \mathrm{SubRing}\left(S\right)\to 0_S=0_U$$
45	12 44	syl	$$⊢\phi \to 0_S=0_U$$
46	45	oveq2d	$$⊢\phi \to F\mathrm{supp}{0}_S=F\mathrm{supp}{0}_U$$
47		eqid	$$⊢0_U=0_U$$
48	2 47 4 10 19 13 14	mhpdeg	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
49	48 5	sseqtrrdi	$$⊢\phi \to F\mathrm{supp}{0}_U\subseteq G$$
50	46 49	eqsstrd	$$⊢\phi \to F\mathrm{supp}{0}_S\subseteq G$$
51		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
52	35 50 27 51	suppssr	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to F\left(b\right)=0_S$$
53	52	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)$$
54	23	adantr	$$⊢\left(\phi \wedge b\in \left(D\setminus G\right)\right)\to S\in \mathrm{Ring}$$
55		eldifi	$$⊢b\in \left(D\setminus G\right)\to b\in D$$
56	55 41	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$$
57	6 9 22 54 56	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$$
58	53 57	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$$
59	58 27	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$$
60	4 16 3 17 6 7 8 9 10 11 12 20 15	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)$$
61	6 22 24 27 43 59 60	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)$$
62	5	ssrab3	$$⊢G\subseteq D$$
63	62	a1i	$$⊢\phi \to G\subseteq D$$
64	63	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)$$
65	64	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)$$
66	21 61 65	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)$$