Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsvarval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsvarval.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsvarval.v	$$⊢V=I\mathrm{mVar}U$$
	evlsvarval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsvarval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsvarval.b	$$⊢B={\mathrm{Base}}_P$$
	evlsvarval.i	$$⊢\phi \to I\in W$$
	evlsvarval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsvarval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsvarval.x	$$⊢\phi \to X\in I$$
	evlsvarval.a	$$⊢\phi \to A\in \left(K^I\right)$$
Assertion	evlsvarval	$$⊢\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		evlsvarval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsvarval.p	$$⊢P=I\mathrm{mPoly}U$$
3		evlsvarval.v	$$⊢V=I\mathrm{mVar}U$$
4		evlsvarval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evlsvarval.k	$$⊢K={\mathrm{Base}}_S$$
6		evlsvarval.b	$$⊢B={\mathrm{Base}}_P$$
7		evlsvarval.i	$$⊢\phi \to I\in W$$
8		evlsvarval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evlsvarval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evlsvarval.x	$$⊢\phi \to X\in I$$
11		evlsvarval.a	$$⊢\phi \to A\in \left(K^I\right)$$
12	4	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
13	9 12	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
14	2 3 6 7 13 10	mvrcl	$$⊢\phi \to V\left(X\right)\in B$$
15		fveq1	$$⊢g=A\to g\left(X\right)=A\left(X\right)$$
16	1 3 4 5 7 8 9 10	evlsvar	$$⊢\phi \to Q\left(V\left(X\right)\right)=\left(g\in \left(K^I\right)⟼g\left(X\right)\right)$$
17		fvexd	$$⊢\phi \to A\left(X\right)\in \mathrm{V}$$
18	15 16 11 17	fvmptd4	$$⊢\phi \to Q\left(V\left(X\right)\right)\left(A\right)=A\left(X\right)$$
19	14 18	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)$$