Theorem evl1scvarpwval

Description: Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-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$$
	evl1scvarpw.t1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
	evl1scvarpw.a	$$⊢\phi \to A\in B$$
	evl1scvarpwval.c	$$⊢\phi \to C\in B$$
	evl1scvarpwval.h	$$⊢H={\mathrm{mulGrp}}_R$$
	evl1scvarpwval.e	$$⊢E={\cdot }_H$$
	evl1scvarpwval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	evl1scvarpwval	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)=A\underset{\dot{}}{·}\left(NEC\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		evl1scvarpw.t1	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
10		evl1scvarpw.a	$$⊢\phi \to A\in B$$
11		evl1scvarpwval.c	$$⊢\phi \to C\in B$$
12		evl1scvarpwval.h	$$⊢H={\mathrm{mulGrp}}_R$$
13		evl1scvarpwval.e	$$⊢E={\cdot }_H$$
14		evl1scvarpwval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
15		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
16		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
17	7 16	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
18	2	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
19	17 18	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
20	3	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
21	19 20	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
22	4 2 15	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
23	17 22	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
24	3 15	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
25	24 6	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in {\mathrm{Base}}_W\right)\to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
26	21 8 23 25	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
27	1 2 3 4 5 6 7 8 11 12 13	evl1varpwval	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)\left(C\right)=NEC$$
28	26 27	jca	$$⊢\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)$$
29	1 2 5 15 7 11 28 10 9 14	evl1vsd	$$⊢\phi \to \left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\in {\mathrm{Base}}_W\wedge Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)=A\underset{\dot{}}{·}\left(NEC\right)\right)$$
30	29	simprd	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)\left(C\right)=A\underset{\dot{}}{·}\left(NEC\right)$$