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=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsbagval.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsbagval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsbagval.w	$$⊢W={\mathrm{Base}}_P$$
	evlsbagval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsbagval.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evlsbagval.e	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsbagval.z	$$⊢\underset{\dot{}}{0}=0_U$$
	evlsbagval.o	$$⊢\underset{\dot{}}{1}=1_U$$
	evlsbagval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsbagval.f	$$⊢F=\left(s\in D⟼if\left(s=B,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
	evlsbagval.i	$$⊢\phi \to I\in V$$
	evlsbagval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsbagval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsbagval.a	$$⊢\phi \to A\in \left(K^I\right)$$
	evlsbagval.b	$$⊢\phi \to B\in D$$
Assertion	evlsbagval	$$⊢\phi \to \left(F\in W\wedge Q\left(F\right)\left(A\right)=\underset{v\in I}{{\sum }_M}\left(B\left(v\right)\underset{\dot{}}{\times }A\left(v\right)\right)\right)$$

Proof

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