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	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsmhpvvval.p	⊢ 𝐻 = ( 𝐼 mHomP 𝑈 )
	evlsmhpvvval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsmhpvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlsmhpvvval.g	⊢ 𝐺 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
	evlsmhpvvval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsmhpvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
	evlsmhpvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
	evlsmhpvvval.x	⊢ · = ( .r ‘ 𝑆 )
	evlsmhpvvval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsmhpvvval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsmhpvvval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
	evlsmhpvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlsmhpvvval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsmhpvvval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsmhpvvval.p	⊢ 𝐻 = ( 𝐼 mHomP 𝑈 )
3		evlsmhpvvval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlsmhpvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5		evlsmhpvvval.g	⊢ 𝐺 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
6		evlsmhpvvval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
7		evlsmhpvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
8		evlsmhpvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
9		evlsmhpvvval.x	⊢ · = ( .r ‘ 𝑆 )
10		evlsmhpvvval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
11		evlsmhpvvval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12		evlsmhpvvval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
13		evlsmhpvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
14		eqid	⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly 𝑈 )
15		eqid	⊢ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑈 ) )
16		reldmmhp	⊢ Rel dom mHomP
17	16 2 12	elfvov1	⊢ ( 𝜑 → 𝐼 ∈ V )
18	2 14 15 12	mhpmpl	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
19	1 14 15 3 4 6 7 8 9 17 10 11 18 13	evlsvvval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
20		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
21	10	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
22	21	ringcmnd	⊢ ( 𝜑 → 𝑆 ∈ CMnd )
23		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
24	4 23	rabex2	⊢ 𝐷 ∈ V
25	24	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
26	21	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
27		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
28	14 27 15 4 18	mplelf	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
29	3	subrgbas	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
30	6	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
31	29 30	eqsstrrd	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
32	11 31	syl	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
33	28 32	fssd	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 )
34	33	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 )
35	17	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ V )
36	10	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
37	13	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
38		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
39	4 6 7 8 35 36 37 38	evlsvvvallem	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
40	6 9 26 34 39	ringcld	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ∈ 𝐾 )
41	40	fmpttd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) : 𝐷 ⟶ 𝐾 )
42	3 20	subrg0	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
43	11 42	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
44	43	oveq2d	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑆 ) ) = ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
45		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
46	2 45 4 12	mhpdeg	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
47	46 5	sseqtrrdi	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ 𝐺 )
48	44 47	eqsstrd	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑆 ) ) ⊆ 𝐺 )
49		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
50	33 48 25 49	suppssr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
51	50	oveq1d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
52	21	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → 𝑆 ∈ Ring )
53		eldifi	⊢ ( 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) → 𝑏 ∈ 𝐷 )
54	53 39	sylan2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
55	6 9 20 52 54	ringlzd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
56	51 55	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
57	56 25	suppss2	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ 𝐺 )
58	4 14 3 15 6 7 8 9 17 10 11 18 13	evlsvvvallem2	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
59	6 20 22 25 41 57 58	gsumres	⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
60	5	ssrab3	⊢ 𝐺 ⊆ 𝐷
61	60	a1i	⊢ ( 𝜑 → 𝐺 ⊆ 𝐷 )
62	61	resmptd	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) = ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) )
63	62	oveq2d	⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
64	19 59 63	3eqtr2d	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )