Theorem evlsvval

Description: Give a formula for the evaluation of a polynomial. (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	evlsvval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsvval.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsvval.b	$$⊢B={\mathrm{Base}}_P$$
	evlsvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	evlsvval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsvval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsvval.t	$$⊢T=S{\uparrow }_{𝑠}\left(K^I\right)$$
	evlsvval.m	$$⊢M={\mathrm{mulGrp}}_T$$
	evlsvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	evlsvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	evlsvval.f	$$⊢F=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)$$
	evlsvval.g	$$⊢G=\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)$$
	evlsvval.i	$$⊢\phi \to I\in V$$
	evlsvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsvval.a	$$⊢\phi \to A\in B$$
Assertion	evlsvval	$$⊢\phi \to Q\left(A\right)=\underset{b\in D}{{\sum }_T}\left(F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlsvval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsvval.p	$$⊢P=I\mathrm{mPoly}U$$
3		evlsvval.b	$$⊢B={\mathrm{Base}}_P$$
4		evlsvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		evlsvval.k	$$⊢K={\mathrm{Base}}_S$$
6		evlsvval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
7		evlsvval.t	$$⊢T=S{\uparrow }_{𝑠}\left(K^I\right)$$
8		evlsvval.m	$$⊢M={\mathrm{mulGrp}}_T$$
9		evlsvval.w	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
10		evlsvval.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
11		evlsvval.f	$$⊢F=\left(x\in R⟼\left(K^I\right)\times \left\{x\right\}\right)$$
12		evlsvval.g	$$⊢G=\left(x\in I⟼\left(a\in \left(K^I\right)⟼a\left(x\right)\right)\right)$$
13		evlsvval.i	$$⊢\phi \to I\in V$$
14		evlsvval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
15		evlsvval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
16		evlsvval.a	$$⊢\phi \to A\in B$$
17		fveq1	$$⊢p=A\to p\left(b\right)=A\left(b\right)$$
18	17	fveq2d	$$⊢p=A\to F\left(p\left(b\right)\right)=F\left(A\left(b\right)\right)$$
19	18	oveq1d	$$⊢p=A\to F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)=F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)$$
20	19	mpteq2dv	$$⊢p=A\to \left(b\in D⟼F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\left(b\in D⟼F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
21	20	oveq2d	$$⊢p=A\to \underset{b\in D}{{\sum }_T}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)=\underset{b\in D}{{\sum }_T}\left(F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$
22		eqid	$$⊢\left(p\in B⟼\underset{b\in D}{{\sum }_T}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)=\left(p\in B⟼\underset{b\in D}{{\sum }_T}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
23	1 2 3 4 5 6 7 8 9 10 22 11 12 13 14 15	evlsval3	$$⊢\phi \to Q=\left(p\in B⟼\underset{b\in D}{{\sum }_T}\left(F\left(p\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\right)$$
24		ovexd	$$⊢\phi \to \underset{b\in D}{{\sum }_T}\left(F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)\in \mathrm{V}$$
25	21 23 16 24	fvmptd4	$$⊢\phi \to Q\left(A\right)=\underset{b\in D}{{\sum }_T}\left(F\left(A\left(b\right)\right)\underset{\dot{}}{·}\left({\sum }_M,\left(b{\underset{\dot{}}{\times }}_{f}G\right)\right)\right)$$