Theorem evls1varpwval

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025)

	Ref	Expression
Hypotheses	evls1varpwval.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1varpwval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1varpwval.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1varpwval.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
	evls1varpwval.b	$$⊢B={\mathrm{Base}}_S$$
	evls1varpwval.e	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_W}$$
	evls1varpwval.f	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	evls1varpwval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1varpwval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1varpwval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	evls1varpwval.c	$$⊢\phi \to C\in B$$
Assertion	evls1varpwval	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }X\right)\left(C\right)=N\underset{\dot{}}{\times }C$$

Proof

Step	Hyp	Ref	Expression
1		evls1varpwval.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1varpwval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
3		evls1varpwval.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1varpwval.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
5		evls1varpwval.b	$$⊢B={\mathrm{Base}}_S$$
6		evls1varpwval.e	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_W}$$
7		evls1varpwval.f	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
8		evls1varpwval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1varpwval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1varpwval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		evls1varpwval.c	$$⊢\phi \to C\in B$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13	2	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
14	4 3 12	vr1cl	$$⊢U\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
15	9 13 14	3syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
16	1 5 3 2 12 8 9 6 7 10 15 11	evls1expd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }X\right)\left(C\right)=N\underset{\dot{}}{\times }Q\left(X\right)\left(C\right)$$
17	1 4 2 5 8 9	evls1var	$$⊢\phi \to Q\left(X\right)={\mathrm{I}\upharpoonright }_B$$
18	17	fveq1d	$$⊢\phi \to Q\left(X\right)\left(C\right)=\left({\mathrm{I}\upharpoonright }_B\right)\left(C\right)$$
19		fvresi	$$⊢C\in B\to \left({\mathrm{I}\upharpoonright }_B\right)\left(C\right)=C$$
20	11 19	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_B\right)\left(C\right)=C$$
21	18 20	eqtrd	$$⊢\phi \to Q\left(X\right)\left(C\right)=C$$
22	21	oveq2d	$$⊢\phi \to N\underset{\dot{}}{\times }Q\left(X\right)\left(C\right)=N\underset{\dot{}}{\times }C$$
23	16 22	eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }X\right)\left(C\right)=N\underset{\dot{}}{\times }C$$