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	3 15	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
17		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
18	7 17	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
19	2	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
20	18 19	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
21	3	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
22	20 21	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
23	4 2 15	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
24	18 23	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
25	16 6 22 8 24	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
26	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$$
27	25 26	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)$$
28	1 2 5 15 7 11 27 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)$$
29	28	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)$$