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		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
24	7 23	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
25	2	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
26	24 25	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
27	3	ringmgp	$$⊢W\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
28	26 27	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
29		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
30	4 2 29	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_W$$
31	24 30	syl	$$⊢\phi \to X\in {\mathrm{Base}}_W$$
32	3 29	mgpbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
33	32 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$$
34	28 8 31 33	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_W$$
35		eqid	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(W\right)$$
36		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
37		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
38		eqid	$$⊢{\cdot }_W={\cdot }_W$$
39	35 36 37 29 38 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)$$
40	16 22 34 39	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)$$
41	40	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)$$
42	41	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)$$
43	1 2 11 5	evl1rhm	$$⊢R\in \mathrm{CRing}\to Q\in \left(W\mathrm{RingHom}S\right)$$
44	7 43	syl	$$⊢\phi \to Q\in \left(W\mathrm{RingHom}S\right)$$
45	2	ply1lmod	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
46	24 45	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
47	35 36 26 46 37 29	asclf	$$⊢\phi \to \mathrm{algSc}\left(W\right):{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟶{\mathrm{Base}}_W$$
48	47 22	ffvelrnd	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(A\right)\in {\mathrm{Base}}_W$$
49	29 38 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)$$
50	44 48 34 49	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)$$
51	1 2 5 35	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\}$$
52	7 10 51	syl2anc	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(A\right)\right)=B\times \left\{A\right\}$$
53	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)$$
54	11	fveq2i	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
55	13 54	eqtri	$$⊢M={\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
56	55	fveq2i	$$⊢{\cdot }_M={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
57	14 56	eqtri	$$⊢F={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
58	57	a1i	$$⊢\phi \to F={\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}$$
59	58	eqcomd	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}=F$$
60	59	oveqd	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{\left(R{\uparrow }_{𝑠}B\right)}}Q\left(X\right)=NFQ\left(X\right)$$
61	53 60	eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=NFQ\left(X\right)$$
62	52 61	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)$$
63	42 50 62	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)$$