Theorem evls1varpw

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		evls1varpw.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1varpw.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
3		evls1varpw.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1varpw.g	$$⊢G={\mathrm{mulGrp}}_W$$
5		evls1varpw.x	$$⊢X={\mathrm{var}}_1\left(U\right)$$
6		evls1varpw.b	$$⊢B={\mathrm{Base}}_S$$
7		evls1varpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
8		evls1varpw.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1varpw.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1varpw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12	2	subrgring	$$⊢R\in \mathrm{SubRing}\left(S\right)\to U\in \mathrm{Ring}$$
13	5 3 11	vr1cl	$$⊢U\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
14	9 12 13	3syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
15	1 2 3 4 6 11 7 8 9 10 14	evls1pw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}B\right)}}Q\left(X\right)$$