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 = ( ( I evalSub S ) ` R )
	evlsvarpw.w	|- W = ( I mPoly U )
	evlsvarpw.g	|- G = ( mulGrp ` W )
	evlsvarpw.e	|- .^ = ( .g ` G )
	evlsvarpw.x	|- X = ( ( I mVar U ) ` Y )
	evlsvarpw.u	|- U = ( S |`s R )
	evlsvarpw.p	|- P = ( S ^s ( B ^m I ) )
	evlsvarpw.h	|- H = ( mulGrp ` P )
	evlsvarpw.b	|- B = ( Base ` S )
	evlsvarpw.i	|- ( ph -> I e. V )
	evlsvarpw.y	|- ( ph -> Y e. I )
	evlsvarpw.s	|- ( ph -> S e. CRing )
	evlsvarpw.r	|- ( ph -> R e. ( SubRing ` S ) )
	evlsvarpw.n	|- ( ph -> N e. NN0 )
Assertion	evlsvarpw	|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvarpw.q	|- Q = ( ( I evalSub S ) ` R )
2		evlsvarpw.w	|- W = ( I mPoly U )
3		evlsvarpw.g	|- G = ( mulGrp ` W )
4		evlsvarpw.e	|- .^ = ( .g ` G )
5		evlsvarpw.x	|- X = ( ( I mVar U ) ` Y )
6		evlsvarpw.u	|- U = ( S |`s R )
7		evlsvarpw.p	|- P = ( S ^s ( B ^m I ) )
8		evlsvarpw.h	|- H = ( mulGrp ` P )
9		evlsvarpw.b	|- B = ( Base ` S )
10		evlsvarpw.i	|- ( ph -> I e. V )
11		evlsvarpw.y	|- ( ph -> Y e. I )
12		evlsvarpw.s	|- ( ph -> S e. CRing )
13		evlsvarpw.r	|- ( ph -> R e. ( SubRing ` S ) )
14		evlsvarpw.n	|- ( ph -> N e. NN0 )
15		eqid	|- ( Base ` W ) = ( Base ` W )
16		eqid	|- ( I mVar U ) = ( I mVar U )
17	6	subrgring	|- ( R e. ( SubRing ` S ) -> U e. Ring )
18	13 17	syl	|- ( ph -> U e. Ring )
19	2 16 15 10 18 11	mvrcl	|- ( ph -> ( ( I mVar U ) ` Y ) e. ( Base ` W ) )
20	5 19	eqeltrid	|- ( ph -> X e. ( Base ` W ) )
21	1 2 3 4 6 7 8 9 15 10 12 13 14 20	evlspw	|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) )