Theorem evls1pw

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024)

	Ref	Expression
Hypotheses	evls1pw.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1pw.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1pw.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1pw.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evls1pw.k	$$⊢K={\mathrm{Base}}_S$$
	evls1pw.b	$$⊢B={\mathrm{Base}}_W$$
	evls1pw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	evls1pw.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1pw.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1pw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	evls1pw.x	$$⊢\phi \to X\in B$$
Assertion	evls1pw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		evls1pw.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1pw.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
3		evls1pw.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1pw.g	$$⊢G={\mathrm{mulGrp}}_W$$
5		evls1pw.k	$$⊢K={\mathrm{Base}}_S$$
6		evls1pw.b	$$⊢B={\mathrm{Base}}_W$$
7		evls1pw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
8		evls1pw.s	$$⊢\phi \to S\in \mathrm{CRing}$$
9		evls1pw.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
10		evls1pw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		evls1pw.x	$$⊢\phi \to X\in B$$
12		eqid	$$⊢S{\uparrow }_{𝑠}K=S{\uparrow }_{𝑠}K$$
13	1 5 12 2 3	evls1rhm	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
14	8 9 13	syl2anc	$$⊢\phi \to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
15		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
16	4 15	rhmmhm	$$⊢Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)\to Q\in \left(G\mathrm{MndHom}{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}\right)$$
17	14 16	syl	$$⊢\phi \to Q\in \left(G\mathrm{MndHom}{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}\right)$$
18	4 6	mgpbas	$$⊢B={\mathrm{Base}}_G$$
19		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}$$
20	18 7 19	mhmmulg	$$⊢\left(Q\in \left(G\mathrm{MndHom}{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}\right)\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(X\right)$$
21	17 10 11 20	syl3anc	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(X\right)$$