Theorem evlvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025)

	Ref	Expression
Hypotheses	evlvvval.q	$$⊢Q=I\mathrm{eval}R$$
	evlvvval.p	$$⊢P=I\mathrm{mPoly}R$$
	evlvvval.b	$$⊢B={\mathrm{Base}}_P$$
	evlvvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlvvval.k	$$⊢K={\mathrm{Base}}_R$$
	evlvvval.m	$$⊢M={\mathrm{mulGrp}}_R$$
	evlvvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlvvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	evlvvval.i	$$⊢\phi \to I\in V$$
	evlvvval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlvvval.f	$$⊢\phi \to F\in B$$
	evlvvval.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	evlvvval	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{b\in D}{{\sum }_R}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlvvval.q	$$⊢Q=I\mathrm{eval}R$$
2		evlvvval.p	$$⊢P=I\mathrm{mPoly}R$$
3		evlvvval.b	$$⊢B={\mathrm{Base}}_P$$
4		evlvvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		evlvvval.k	$$⊢K={\mathrm{Base}}_R$$
6		evlvvval.m	$$⊢M={\mathrm{mulGrp}}_R$$
7		evlvvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
8		evlvvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9		evlvvval.i	$$⊢\phi \to I\in V$$
10		evlvvval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
11		evlvvval.f	$$⊢\phi \to F\in B$$
12		evlvvval.a	$$⊢\phi \to A\in \left(K^I\right)$$
13		eqid	$$⊢\left(I\mathrm{evalSub}R\right)\left({\mathrm{Base}}_R\right)=\left(I\mathrm{evalSub}R\right)\left({\mathrm{Base}}_R\right)$$
14		eqid	$$⊢I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)=I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)$$
15		eqid	$$⊢R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R$$
16		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\right)}$$
17	10	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
18		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
19	18	subrgid	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_R\in \mathrm{SubRing}\left(R\right)$$
20	17 19	syl	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{SubRing}\left(R\right)$$
21	18	ressid	$$⊢R\in \mathrm{CRing}\to R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R$$
22	10 21	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R=R$$
23	22	oveq2d	$$⊢\phi \to I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)=I\mathrm{mPoly}R$$
24	23 2	eqtr4di	$$⊢\phi \to I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)=P$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\right)}={\mathrm{Base}}_P$$
26	25 3	eqtr4di	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\right)}=B$$
27	11 26	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}\left(R{\upharpoonright }_{𝑠}{\mathrm{Base}}_R\right)\right)}$$
28	13 1 14 15 16 9 10 20 27	evlsevl	$$⊢\phi \to \left(I\mathrm{evalSub}R\right)\left({\mathrm{Base}}_R\right)\left(F\right)=Q\left(F\right)$$
29	28	fveq1d	$$⊢\phi \to \left(I\mathrm{evalSub}R\right)\left({\mathrm{Base}}_R\right)\left(F\right)\left(A\right)=Q\left(F\right)\left(A\right)$$
30	13 14 16 15 4 5 6 7 8 9 10 20 27 12	evlsvvval	$$⊢\phi \to \left(I\mathrm{evalSub}R\right)\left({\mathrm{Base}}_R\right)\left(F\right)\left(A\right)=\underset{b\in D}{{\sum }_R}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$
31	29 30	eqtr3d	$$⊢\phi \to Q\left(F\right)\left(A\right)=\underset{b\in D}{{\sum }_R}\left(F\left(b\right)\underset{\dot{}}{·}\left(\underset{i\in I}{{\sum }_M},\left(b\left(i\right)\underset{\dot{}}{\times }A\left(i\right)\right)\right)\right)$$