This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = { ℎ ∈ ( ℕ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 ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )