Theorem evls1scafv

Description: Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025)

	Ref	Expression
Hypotheses	evls1scafv.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1scafv.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1scafv.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1scafv.b	$$⊢B={\mathrm{Base}}_S$$
	evls1scafv.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	evls1scafv.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1scafv.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1scafv.x	$$⊢\phi \to X\in R$$
	evls1scafv.1	$$⊢\phi \to C\in B$$
Assertion	evls1scafv	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(C\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		evls1scafv.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1scafv.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
3		evls1scafv.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evls1scafv.b	$$⊢B={\mathrm{Base}}_S$$
5		evls1scafv.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
6		evls1scafv.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evls1scafv.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8		evls1scafv.x	$$⊢\phi \to X\in R$$
9		evls1scafv.1	$$⊢\phi \to C\in B$$
10	1 2 3 4 5 6 7 8	evls1sca	$$⊢\phi \to Q\left(A\left(X\right)\right)=B\times \left\{X\right\}$$
11	10	fveq1d	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(C\right)=\left(B\times \left\{X\right\}\right)\left(C\right)$$
12		fvconst2g	$$⊢\left(X\in R\wedge C\in B\right)\to \left(B\times \left\{X\right\}\right)\left(C\right)=X$$
13	8 9 12	syl2anc	$$⊢\phi \to \left(B\times \left\{X\right\}\right)\left(C\right)=X$$
14	11 13	eqtrd	$$⊢\phi \to Q\left(A\left(X\right)\right)\left(C\right)=X$$