Theorem evlspw

Description: 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	evlspw.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlspw.w	$$⊢W=I\mathrm{mPoly}U$$
	evlspw.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evlspw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	evlspw.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlspw.p	$$⊢P=S{\uparrow }_{𝑠}\left(K^I\right)$$
	evlspw.h	$$⊢H={\mathrm{mulGrp}}_P$$
	evlspw.k	$$⊢K={\mathrm{Base}}_S$$
	evlspw.b	$$⊢B={\mathrm{Base}}_W$$
	evlspw.i	$$⊢\phi \to I\in V$$
	evlspw.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlspw.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlspw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	evlspw.x	$$⊢\phi \to X\in B$$
Assertion	evlspw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{H}Q\left(X\right)$$

Proof

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