Metamath Proof Explorer

Theorem evlsbagval

Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since .0. and .1. using U instead of S may not be convenient. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses evlsbagval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsbagval.p 
|- P = ( I mPoly U )
evlsbagval.u 
|- U = ( S |`s R )
evlsbagval.w 
|- W = ( Base ` P )
evlsbagval.k 
|- K = ( Base ` S )
evlsbagval.m 
|- M = ( mulGrp ` S )
evlsbagval.e 
|- .^ = ( .g ` M )
evlsbagval.z 
|- .0. = ( 0g ` U )
evlsbagval.o 
|- .1. = ( 1r ` U )
evlsbagval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlsbagval.f 
|- F = ( s e. D |-> if ( s = B , .1. , .0. ) )
evlsbagval.i 
|- ( ph -> I e. V )
evlsbagval.s 
|- ( ph -> S e. CRing )
evlsbagval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsbagval.a 
|- ( ph -> A e. ( K ^m I ) )
evlsbagval.b 
|- ( ph -> B e. D )
Assertion evlsbagval 
|- ( ph -> ( F e. W /\ ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evlsbagval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsbagval.p 
 |-  P = ( I mPoly U )
3 evlsbagval.u 
 |-  U = ( S |`s R )
4 evlsbagval.w 
 |-  W = ( Base ` P )
5 evlsbagval.k 
 |-  K = ( Base ` S )
6 evlsbagval.m 
 |-  M = ( mulGrp ` S )
7 evlsbagval.e 
 |-  .^ = ( .g ` M )
8 evlsbagval.z 
 |-  .0. = ( 0g ` U )
9 evlsbagval.o 
 |-  .1. = ( 1r ` U )
10 evlsbagval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 evlsbagval.f 
 |-  F = ( s e. D |-> if ( s = B , .1. , .0. ) )
12 evlsbagval.i 
 |-  ( ph -> I e. V )
13 evlsbagval.s 
 |-  ( ph -> S e. CRing )
14 evlsbagval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
15 evlsbagval.a 
 |-  ( ph -> A e. ( K ^m I ) )
16 evlsbagval.b 
 |-  ( ph -> B e. D )
17 fvexd 
 |-  ( ph -> ( Base ` U ) e. _V )
18 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
19 10 18 rabexd 
 |-  ( ph -> D e. _V )
20 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
21 14 20 syl 
 |-  ( ph -> U e. Ring )
22 eqid 
 |-  ( Base ` U ) = ( Base ` U )
23 22 9 ringidcl 
 |-  ( U e. Ring -> .1. e. ( Base ` U ) )
24 21 23 syl 
 |-  ( ph -> .1. e. ( Base ` U ) )
25 22 8 ring0cl 
 |-  ( U e. Ring -> .0. e. ( Base ` U ) )
26 21 25 syl 
 |-  ( ph -> .0. e. ( Base ` U ) )
27 24 26 ifcld 
 |-  ( ph -> if ( s = B , .1. , .0. ) e. ( Base ` U ) )
28 27 adantr 
 |-  ( ( ph /\ s e. D ) -> if ( s = B , .1. , .0. ) e. ( Base ` U ) )
29 28 11 fmptd 
 |-  ( ph -> F : D --> ( Base ` U ) )
30 17 19 29 elmapdd 
 |-  ( ph -> F e. ( ( Base ` U ) ^m D ) )
31 eqid 
 |-  ( I mPwSer U ) = ( I mPwSer U )
32 eqid 
 |-  ( Base ` ( I mPwSer U ) ) = ( Base ` ( I mPwSer U ) )
33 31 22 10 32 12 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer U ) ) = ( ( Base ` U ) ^m D ) )
34 30 33 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( I mPwSer U ) ) )
35 19 26 11 sniffsupp 
 |-  ( ph -> F finSupp .0. )
36 2 31 32 8 4 mplelbas 
 |-  ( F e. W <-> ( F e. ( Base ` ( I mPwSer U ) ) /\ F finSupp .0. ) )
37 34 35 36 sylanbrc 
 |-  ( ph -> F e. W )
38 eqid 
 |-  ( .r ` S ) = ( .r ` S )
39 1 2 4 3 10 5 6 7 38 12 13 14 37 15 evlsvvval 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( S gsum ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) )
40 16 snssd 
 |-  ( ph -> { B } C_ D )
41 resmpt 
 |-  ( { B } C_ D -> ( ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |` { B } ) = ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) )
42 40 41 syl 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |` { B } ) = ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) )
43 42 oveq2d 
 |-  ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |` { B } ) ) = ( S gsum ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) )
44 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
45 13 crngringd 
 |-  ( ph -> S e. Ring )
46 45 ringcmnd 
 |-  ( ph -> S e. CMnd )
47 45 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. Ring )
48 3 subrgbas 
 |-  ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
49 5 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
50 48 49 eqsstrrd 
 |-  ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K )
51 14 50 syl 
 |-  ( ph -> ( Base ` U ) C_ K )
52 29 51 fssd 
 |-  ( ph -> F : D --> K )
53 52 ffvelcdmda 
 |-  ( ( ph /\ b e. D ) -> ( F ` b ) e. K )
54 12 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. V )
55 13 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. CRing )
56 15 adantr 
 |-  ( ( ph /\ b e. D ) -> A e. ( K ^m I ) )
57 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
58 10 5 6 7 54 55 56 57 evlsvvvallem 
 |-  ( ( ph /\ b e. D ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
59 5 38 47 53 58 ringcld 
 |-  ( ( ph /\ b e. D ) -> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) e. K )
60 59 fmpttd 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) : D --> K )
61 eldifsnneq 
 |-  ( b e. ( D \ { B } ) -> -. b = B )
62 61 adantl 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> -. b = B )
63 62 iffalsed 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> if ( b = B , .1. , .0. ) = .0. )
64 eqeq1 
 |-  ( s = b -> ( s = B <-> b = B ) )
65 64 ifbid 
 |-  ( s = b -> if ( s = B , .1. , .0. ) = if ( b = B , .1. , .0. ) )
66 eldifi 
 |-  ( b e. ( D \ { B } ) -> b e. D )
67 66 adantl 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> b e. D )
68 9 fvexi 
 |-  .1. e. _V
69 8 fvexi 
 |-  .0. e. _V
70 68 69 ifex 
 |-  if ( b = B , .1. , .0. ) e. _V
71 70 a1i 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> if ( b = B , .1. , .0. ) e. _V )
72 11 65 67 71 fvmptd3 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( F ` b ) = if ( b = B , .1. , .0. ) )
73 3 44 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
74 73 8 eqtr4di 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = .0. )
75 14 74 syl 
 |-  ( ph -> ( 0g ` S ) = .0. )
76 75 adantr 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( 0g ` S ) = .0. )
77 63 72 76 3eqtr4d 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( F ` b ) = ( 0g ` S ) )
78 77 oveq1d 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( ( 0g ` S ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) )
79 66 58 sylan2 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
80 5 38 44 ringlz 
 |-  ( ( S e. Ring /\ ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K ) -> ( ( 0g ` S ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
81 45 79 80 syl2an2r 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( 0g ` S ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
82 78 81 eqtrd 
 |-  ( ( ph /\ b e. ( D \ { B } ) ) -> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
83 82 19 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) supp ( 0g ` S ) ) C_ { B } )
84 10 2 3 4 5 6 7 38 12 13 14 37 15 evlsvvvallem2 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` S ) )
85 5 44 46 19 60 83 84 gsumres 
 |-  ( ph -> ( S gsum ( ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) |` { B } ) ) = ( S gsum ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) )
86 13 crnggrpd 
 |-  ( ph -> S e. Grp )
87 86 grpmndd 
 |-  ( ph -> S e. Mnd )
88 52 16 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. K )
89 10 5 6 7 12 13 15 16 evlsvvvallem 
 |-  ( ph -> ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) e. K )
90 5 38 45 88 89 ringcld 
 |-  ( ph -> ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) e. K )
91 fveq2 
 |-  ( b = B -> ( F ` b ) = ( F ` B ) )
92 fveq1 
 |-  ( b = B -> ( b ` v ) = ( B ` v ) )
93 92 oveq1d 
 |-  ( b = B -> ( ( b ` v ) .^ ( A ` v ) ) = ( ( B ` v ) .^ ( A ` v ) ) )
94 93 mpteq2dv 
 |-  ( b = B -> ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) = ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) )
95 94 oveq2d 
 |-  ( b = B -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
96 91 95 oveq12d 
 |-  ( b = B -> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )
97 5 96 gsumsn 
 |-  ( ( S e. Mnd /\ B e. D /\ ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) e. K ) -> ( S gsum ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) = ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )
98 87 16 90 97 syl3anc 
 |-  ( ph -> ( S gsum ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) = ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )
99 iftrue 
 |-  ( s = B -> if ( s = B , .1. , .0. ) = .1. )
100 68 a1i 
 |-  ( ph -> .1. e. _V )
101 11 99 16 100 fvmptd3 
 |-  ( ph -> ( F ` B ) = .1. )
102 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
103 3 102 subrg1 
 |-  ( R e. ( SubRing ` S ) -> ( 1r ` S ) = ( 1r ` U ) )
104 14 103 syl 
 |-  ( ph -> ( 1r ` S ) = ( 1r ` U ) )
105 9 101 104 3eqtr4a 
 |-  ( ph -> ( F ` B ) = ( 1r ` S ) )
106 105 oveq1d 
 |-  ( ph -> ( ( F ` B ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) = ( ( 1r ` S ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )
107 5 38 102 45 89 ringlidmd 
 |-  ( ph -> ( ( 1r ` S ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
108 98 106 107 3eqtrd 
 |-  ( ph -> ( S gsum ( b e. { B } |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
109 43 85 108 3eqtr3d 
 |-  ( ph -> ( S gsum ( b e. D |-> ( ( F ` b ) ( .r ` S ) ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
110 39 109 eqtrd 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) )
111 37 110 jca 
 |-  ( ph -> ( F e. W /\ ( ( Q ` F ) ` A ) = ( M gsum ( v e. I |-> ( ( B ` v ) .^ ( A ` v ) ) ) ) ) )