Theorem evl1varpw

Description: Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd , the proof is shorter using evls1varpw instead of proving it directly. (Contributed by AV, 15-Sep-2019)

	Ref	Expression
Hypotheses	evl1varpw.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
	evl1varpw.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	evl1varpw.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evl1varpw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	evl1varpw.b	$$⊢B={\mathrm{Base}}_R$$
	evl1varpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	evl1varpw.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1varpw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	evl1varpw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1varpw.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
2		evl1varpw.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
3		evl1varpw.g	$$⊢G={\mathrm{mulGrp}}_W$$
4		evl1varpw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		evl1varpw.b	$$⊢B={\mathrm{Base}}_R$$
6		evl1varpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
7		evl1varpw.r	$$⊢\phi \to R\in \mathrm{CRing}$$
8		evl1varpw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9	1 5	evl1fval1	$$⊢Q=R{\mathrm{evalSub}}_{1}B$$
10	9	a1i	$$⊢\phi \to Q=R{\mathrm{evalSub}}_{1}B$$
11	2	fveq2i	$$⊢{\mathrm{mulGrp}}_W={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}$$
12	3 11	eqtri	$$⊢G={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}$$
13	12	fveq2i	$$⊢{\cdot }_G={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
14	6 13	eqtri	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}$$
15	5	ressid	$$⊢R\in \mathrm{CRing}\to R{\upharpoonright }_{𝑠}B=R$$
16	7 15	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}B=R$$
17	16	eqcomd	$$⊢\phi \to R=R{\upharpoonright }_{𝑠}B$$
18	17	fveq2d	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
19	18	fveq2d	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}$$
20	19	fveq2d	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}$$
21	14 20	syl5eq	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}$$
22		eqidd	$$⊢\phi \to N=N$$
23	17	fveq2d	$$⊢\phi \to {\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
24	4 23	syl5eq	$$⊢\phi \to X={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
25	21 22 24	oveq123d	$$⊢\phi \to N\underset{\dot{}}{\times }X=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
26	10 25	fveq12d	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=\left(R{\mathrm{evalSub}}_{1}B\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)\right)$$
27		eqid	$$⊢R{\mathrm{evalSub}}_{1}B=R{\mathrm{evalSub}}_{1}B$$
28		eqid	$$⊢R{\upharpoonright }_{𝑠}B=R{\upharpoonright }_{𝑠}B$$
29		eqid	$$⊢{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
30		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}$$
31		eqid	$$⊢{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)$$
32		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}$$
33		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
34	5	subrgid	$$⊢R\in \mathrm{Ring}\to B\in \mathrm{SubRing}\left(R\right)$$
35	7 33 34	3syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(R\right)$$
36	27 28 29 30 31 5 32 7 35 8	evls1varpw	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}B\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}B\right)}}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}\left(R{\mathrm{evalSub}}_{1}B\right)\left({\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)\right)$$
37	9	eqcomi	$$⊢R{\mathrm{evalSub}}_{1}B=Q$$
38	37	a1i	$$⊢\phi \to R{\mathrm{evalSub}}_{1}B=Q$$
39	24	eqcomd	$$⊢\phi \to {\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)=X$$
40	38 39	fveq12d	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}B\right)\left({\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)\right)=Q\left(X\right)$$
41	40	oveq2d	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}\left(R{\mathrm{evalSub}}_{1}B\right)\left({\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}B\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)$$
42	26 36 41	3eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)$$