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