Theorem evl1scvarpw

Description: Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an 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$$
	evl1scvarpw.s	$$⊢S=R{\uparrow }_{𝑠}B$$
	evl1scvarpw.t2	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
	evl1scvarpw.m	$$⊢M={\mathrm{mulGrp}}_S$$
	evl1scvarpw.f	$$⊢F={\cdot }_M$$
Assertion	evl1scvarpw	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)=\left(B\times \left\{A\right\}\right)\underset{\dot{}}{\bullet }\left(NFQ\left(X\right)\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		evl1scvarpw.s	$$⊢S=R{\uparrow }_{𝑠}B$$
12		evl1scvarpw.t2	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
13		evl1scvarpw.m	$$⊢M={\mathrm{mulGrp}}_S$$
14		evl1scvarpw.f	$$⊢F={\cdot }_M$$
15	2	ply1assa	$$⊢R\in \mathrm{CRing}\to W\in \mathrm{AssAlg}$$
16	7 15	syl	$$⊢\phi \to W\in \mathrm{AssAlg}$$
17	10 5	eleqtrdi	$$⊢\phi \to A\in {\mathrm{Base}}_R$$
18	2	ply1sca	$$⊢R\in \mathrm{CRing}\to R=\mathrm{Scalar}\left(W\right)$$
19	18	eqcomd	$$⊢R\in \mathrm{CRing}\to \mathrm{Scalar}\left(W\right)=R$$
20	7 19	syl	$$⊢\phi \to \mathrm{Scalar}\left(W\right)=R$$
21	20	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_R$$
22	17 21	eleqtrrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
23		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
24	3 23	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
25		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
26	7 25	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
27	2	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
28	26 27	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
29	3	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
30	28 29	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
31	4 2 23	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
32	26 31	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
33	24 6 30 8 32	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
34		eqid	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(W\right)$$
35		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
36		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
37		eqid	$$⊢{\cdot }_W={\cdot }_W$$
38	34 35 36 23 37 9	asclmul1	$$⊢\left(W\in \mathrm{AssAlg}\wedge A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W\right)\to \mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)=A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)$$
39	16 22 33 38	syl3anc	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)=A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)$$
40	39	eqcomd	$$⊢\phi \to A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)=\mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)$$
41	40	fveq2d	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)=Q\left(\mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)\right)$$
42	1 2 11 5	evl1rhm	$$⊢R\in \mathrm{CRing}\to Q\in \left(W\mathrm{RingHom}S\right)$$
43	7 42	syl	$$⊢\phi \to Q\in \left(W\mathrm{RingHom}S\right)$$
44	2	ply1lmod	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
45	26 44	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
46	34 35 28 45 36 23	asclf	$$⊢\phi \to \mathrm{algSc}\left(W\right):{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟶{\mathrm{Base}}_W$$
47	46 22	ffvelcdmd	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(A\right)\in {\mathrm{Base}}_W$$
48	23 37 12	rhmmul	$$⊢\left(Q\in \left(W\mathrm{RingHom}S\right)\wedge \mathrm{algSc}\left(W\right)\left(A\right)\in {\mathrm{Base}}_W\wedge N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W\right)\to Q\left(\mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)\right)=Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)\underset{\dot{}}{\bullet }Q\left(N\underset{\dot{}}{\times }X\right)$$
49	43 47 33 48	syl3anc	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(A\right){\cdot }_W\left(N\underset{\dot{}}{\times }X\right)\right)=Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)\underset{\dot{}}{\bullet }Q\left(N\underset{\dot{}}{\times }X\right)$$
50	1 2 5 34	evl1sca	$$⊢\left(R\in \mathrm{CRing}\wedge A\in B\right)\to Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)=B\times \left\{A\right\}$$
51	7 10 50	syl2anc	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)=B\times \left\{A\right\}$$
52	1 2 3 4 5 6 7 8	evl1varpw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)$$
53	11	fveq2i	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
54	13 53	eqtri	$$⊢M={\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
55	54	fveq2i	$$⊢{\cdot }_M={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
56	14 55	eqtri	$$⊢F={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
57	56	a1i	$$⊢\phi \to F={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
58	57	eqcomd	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}=F$$
59	58	oveqd	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)=NFQ\left(X\right)$$
60	52 59	eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=NFQ\left(X\right)$$
61	51 60	oveq12d	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)\underset{\dot{}}{\bullet }Q\left(N\underset{\dot{}}{\times }X\right)=\left(B\times \left\{A\right\}\right)\underset{\dot{}}{\bullet }\left(NFQ\left(X\right)\right)$$
62	41 49 61	3eqtrd	$$⊢\phi \to Q\left(A\underset{\dot{}}{\times }\left(N\underset{\dot{}}{\times }X\right)\right)=\left(B\times \left\{A\right\}\right)\underset{\dot{}}{\bullet }\left(NFQ\left(X\right)\right)$$