Theorem evlscaval

Description: Polynomial evaluation for scalars. See evlsscaval . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlscafv.1	$$⊢Q=I\mathrm{eval}R$$
	evlscafv.2	$$⊢W=I\mathrm{mPoly}R$$
	evlscafv.3	$$⊢B={\mathrm{Base}}_R$$
	evlscafv.4	$$⊢A=\mathrm{algSc}\left(W\right)$$
	evlscafv.5	$$⊢\phi \to I\in V$$
	evlscafv.6	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlscafv.7	$$⊢\phi \to X\in B$$
	evlscafv.8	$$⊢\phi \to L:I⟶B$$
Assertion	evlscaval	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(L\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		evlscafv.1	$$⊢Q=I\mathrm{eval}R$$
2		evlscafv.2	$$⊢W=I\mathrm{mPoly}R$$
3		evlscafv.3	$$⊢B={\mathrm{Base}}_R$$
4		evlscafv.4	$$⊢A=\mathrm{algSc}\left(W\right)$$
5		evlscafv.5	$$⊢\phi \to I\in V$$
6		evlscafv.6	$$⊢\phi \to R\in \mathrm{CRing}$$
7		evlscafv.7	$$⊢\phi \to X\in B$$
8		evlscafv.8	$$⊢\phi \to L:I⟶B$$
9	1 2 3 4 5 6 7	evlsca	$$⊢\phi \to Q\left(A\left(X\right)\right)=\left(B^I\right)\times \left\{X\right\}$$
10	9	fveq1d	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(L\right)=\left(\left(B^I\right)\times \left\{X\right\}\right)\left(L\right)$$
11	3	fvexi	$$⊢B\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to B\in \mathrm{V}$$
13	12 5 8	elmapdd	$$⊢\phi \to L\in \left(B^I\right)$$
14		fvconst2g	$$⊢\left(X\in B\wedge L\in \left(B^I\right)\right)\to \left(\left(B^I\right)\times \left\{X\right\}\right)\left(L\right)=X$$
15	7 13 14	syl2anc	$$⊢\phi \to \left(\left(B^I\right)\times \left\{X\right\}\right)\left(L\right)=X$$
16	10 15	eqtrd	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(L\right)=X$$