Theorem evl1varpwval

Description: Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-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$$
	evl1varpwval.c	$$⊢\phi \to C\in B$$
	evl1varpwval.h	$$⊢H={\mathrm{mulGrp}}_R$$
	evl1varpwval.e	$$⊢E={\cdot }_H$$
Assertion	evl1varpwval	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)\left(C\right)=NEC$$

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		evl1varpwval.c	$$⊢\phi \to C\in B$$
10		evl1varpwval.h	$$⊢H={\mathrm{mulGrp}}_R$$
11		evl1varpwval.e	$$⊢E={\cdot }_H$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13	1 4 5 2 12 7 9	evl1vard	$$⊢\phi \to \left(X\in {\mathrm{Base}}_W\wedge Q\left(X\right)\left(C\right)=C\right)$$
14	3	fveq2i	$$⊢{\cdot }_G={\cdot }_{{\mathrm{mulGrp}}_W}$$
15	6 14	eqtri	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_W}$$
16	10	fveq2i	$$⊢{\cdot }_H={\cdot }_{{\mathrm{mulGrp}}_R}$$
17	11 16	eqtri	$$⊢E={\cdot }_{{\mathrm{mulGrp}}_R}$$
18	1 2 5 12 7 9 13 15 17 8	evl1expd	$$⊢\phi \to \left(N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W\wedge Q\left(N\underset{\dot{}}{\times }X\right)\left(C\right)=NEC\right)$$
19	18	simprd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)\left(C\right)=NEC$$