Metamath Proof Explorer


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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
evlsmhpvvval.g 𝐺 = { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σ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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
5 evlsmhpvvval.g 𝐺 = { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σ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 ( ℕ0m 𝐼 ) ∈ 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𝑈 ) ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σ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 ( 𝑖𝐼 ↦ ( ( 𝑏𝑖 ) ( 𝐴𝑖 ) ) ) ) ) ) ) )