Theorem evlsvarpw

Description: Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024)

	Ref	Expression
Hypotheses	evlsvarpw.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsvarpw.w	$$⊢W=I\mathrm{mPoly}U$$
	evlsvarpw.g	$$⊢G={\mathrm{mulGrp}}_W$$
	evlsvarpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	evlsvarpw.x	$$⊢X=\left(I\mathrm{mVar}U\right)\left(Y\right)$$
	evlsvarpw.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsvarpw.p	$$⊢P=S{\uparrow }_{𝑠}\left(B^I\right)$$
	evlsvarpw.h	$$⊢H={\mathrm{mulGrp}}_P$$
	evlsvarpw.b	$$⊢B={\mathrm{Base}}_S$$
	evlsvarpw.i	$$⊢\phi \to I\in V$$
	evlsvarpw.y	$$⊢\phi \to Y\in I$$
	evlsvarpw.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsvarpw.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsvarpw.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	evlsvarpw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\times }X\right)=N{\cdot }_{H}Q\left(X\right)$$

Proof

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