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 
|- Q = ( ( I evalSub S ) ` R )
evlsmhpvvval.p 
|- H = ( I mHomP U )
evlsmhpvvval.u 
|- U = ( S |`s R )
evlsmhpvvval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlsmhpvvval.g 
|- G = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
evlsmhpvvval.k 
|- K = ( Base ` S )
evlsmhpvvval.m 
|- M = ( mulGrp ` S )
evlsmhpvvval.w 
|- .^ = ( .g ` M )
evlsmhpvvval.x 
|- .x. = ( .r ` S )
evlsmhpvvval.s 
|- ( ph -> S e. CRing )
evlsmhpvvval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsmhpvvval.f 
|- ( ph -> F e. ( H ` N ) )
evlsmhpvvval.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlsmhpvvval 
|- ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evlsmhpvvval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsmhpvvval.p 
 |-  H = ( I mHomP U )
3 evlsmhpvvval.u 
 |-  U = ( S |`s R )
4 evlsmhpvvval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5 evlsmhpvvval.g 
 |-  G = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
6 evlsmhpvvval.k 
 |-  K = ( Base ` S )
7 evlsmhpvvval.m 
 |-  M = ( mulGrp ` S )
8 evlsmhpvvval.w 
 |-  .^ = ( .g ` M )
9 evlsmhpvvval.x 
 |-  .x. = ( .r ` S )
10 evlsmhpvvval.s 
 |-  ( ph -> S e. CRing )
11 evlsmhpvvval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
12 evlsmhpvvval.f 
 |-  ( ph -> F e. ( H ` N ) )
13 evlsmhpvvval.a 
 |-  ( ph -> A e. ( K ^m I ) )
14 eqid 
 |-  ( I mPoly U ) = ( I mPoly U )
15 eqid 
 |-  ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) )
16 reldmmhp 
 |-  Rel dom mHomP
17 16 2 12 elfvov1 
 |-  ( ph -> I e. _V )
18 2 14 15 12 mhpmpl 
 |-  ( ph -> F e. ( Base ` ( I mPoly U ) ) )
19 1 14 15 3 4 6 7 8 9 17 10 11 18 13 evlsvvval 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
20 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
21 10 crngringd 
 |-  ( ph -> S e. Ring )
22 21 ringcmnd 
 |-  ( ph -> S e. CMnd )
23 ovex 
 |-  ( NN0 ^m I ) e. _V
24 4 23 rabex2 
 |-  D e. _V
25 24 a1i 
 |-  ( ph -> D e. _V )
26 21 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. Ring )
27 eqid 
 |-  ( Base ` U ) = ( Base ` U )
28 14 27 15 4 18 mplelf 
 |-  ( ph -> F : D --> ( Base ` U ) )
29 3 subrgbas 
 |-  ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
30 6 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
31 29 30 eqsstrrd 
 |-  ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K )
32 11 31 syl 
 |-  ( ph -> ( Base ` U ) C_ K )
33 28 32 fssd 
 |-  ( ph -> F : D --> K )
34 33 ffvelcdmda 
 |-  ( ( ph /\ b e. D ) -> ( F ` b ) e. K )
35 17 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. _V )
36 10 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. CRing )
37 13 adantr 
 |-  ( ( ph /\ b e. D ) -> A e. ( K ^m I ) )
38 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
39 4 6 7 8 35 36 37 38 evlsvvvallem 
 |-  ( ( ph /\ b e. D ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K )
40 6 9 26 34 39 ringcld 
 |-  ( ( ph /\ b e. D ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) e. K )
41 40 fmpttd 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) : D --> K )
42 3 20 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
43 11 42 syl 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
44 43 oveq2d 
 |-  ( ph -> ( F supp ( 0g ` S ) ) = ( F supp ( 0g ` U ) ) )
45 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
46 2 45 4 12 mhpdeg 
 |-  ( ph -> ( F supp ( 0g ` U ) ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
47 46 5 sseqtrrdi 
 |-  ( ph -> ( F supp ( 0g ` U ) ) C_ G )
48 44 47 eqsstrd 
 |-  ( ph -> ( F supp ( 0g ` S ) ) C_ G )
49 fvexd 
 |-  ( ph -> ( 0g ` S ) e. _V )
50 33 48 25 49 suppssr 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> ( F ` b ) = ( 0g ` S ) )
51 50 oveq1d 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) )
52 21 adantr 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> S e. Ring )
53 eldifi 
 |-  ( b e. ( D \ G ) -> b e. D )
54 53 39 sylan2 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K )
55 6 9 20 52 54 ringlzd 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> ( ( 0g ` S ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) )
56 51 55 eqtrd 
 |-  ( ( ph /\ b e. ( D \ G ) ) -> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( 0g ` S ) )
57 56 25 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) supp ( 0g ` S ) ) C_ G )
58 4 14 3 15 6 7 8 9 17 10 11 18 13 evlsvvvallem2 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) finSupp ( 0g ` S ) )
59 6 20 22 25 41 57 58 gsumres 
 |-  ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) ) = ( S gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
60 5 ssrab3 
 |-  G C_ D
61 60 a1i 
 |-  ( ph -> G C_ D )
62 61 resmptd 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) = ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) )
63 62 oveq2d 
 |-  ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |` G ) ) = ( S gsum ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
64 19 59 63 3eqtr2d 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. G |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )