Theorem evlvarval

Description: Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlvarval.1	$$⊢Q=I\mathrm{eval}S$$
	evlvarval.2	$$⊢P=I\mathrm{mPoly}S$$
	evlvarval.3	$$⊢K={\mathrm{Base}}_S$$
	evlvarval.4	$$⊢B={\mathrm{Base}}_P$$
	evlvarval.5	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	evlvarval.6	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	evlvarval.7	$$⊢\phi \to I\in Z$$
	evlvarval.8	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlvarval.9	$$⊢\phi \to A\in \left(K^I\right)$$
	evlvarval.10	$$⊢V=I\mathrm{mVar}S$$
	evlvarval.11	$$⊢\phi \to X\in I$$
Assertion	evlvarval	$$⊢\phi \to \left(V\left(X\right)\in B\wedge Q\left(V\left(X\right)\right)\left(A\right)=A\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlvarval.1	$$⊢Q=I\mathrm{eval}S$$
2		evlvarval.2	$$⊢P=I\mathrm{mPoly}S$$
3		evlvarval.3	$$⊢K={\mathrm{Base}}_S$$
4		evlvarval.4	$$⊢B={\mathrm{Base}}_P$$
5		evlvarval.5	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
6		evlvarval.6	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
7		evlvarval.7	$$⊢\phi \to I\in Z$$
8		evlvarval.8	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evlvarval.9	$$⊢\phi \to A\in \left(K^I\right)$$
10		evlvarval.10	$$⊢V=I\mathrm{mVar}S$$
11		evlvarval.11	$$⊢\phi \to X\in I$$
12	8	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
13	2 10 4 7 12 11	mvrcl	$$⊢\phi \to V\left(X\right)\in B$$
14		fveq1	$$⊢a=A\to a\left(X\right)=A\left(X\right)$$
15	1 10 3 7 8 11	evlvar	$$⊢\phi \to Q\left(V\left(X\right)\right)=\left(a\in \left(K^I\right)⟼a\left(X\right)\right)$$
16	3	fvexi	$$⊢K\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to K\in \mathrm{V}$$
18	7 17 9	elmaprd	$$⊢\phi \to A:I⟶K$$
19	18 11	ffvelcdmd	$$⊢\phi \to A\left(X\right)\in K$$
20	14 15 9 19	fvmptd4	$$⊢\phi \to Q\left(V\left(X\right)\right)\left(A\right)=A\left(X\right)$$
21	13 20	jca	$$⊢\phi \to \left(V\left(X\right)\in B\wedge Q\left(V\left(X\right)\right)\left(A\right)=A\left(X\right)\right)$$