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

Proof

Step	Hyp	Ref	Expression
1		evlspw.q	\|- Q = ( ( I evalSub S ) ` R )
2		evlspw.w	\|- W = ( I mPoly U )
3		evlspw.g	\|- G = ( mulGrp ` W )
4		evlspw.e	\|- .^ = ( .g ` G )
5		evlspw.u	\|- U = ( S \|`s R )
6		evlspw.p	\|- P = ( S ^s ( K ^m I ) )
7		evlspw.h	\|- H = ( mulGrp ` P )
8		evlspw.k	\|- K = ( Base ` S )
9		evlspw.b	\|- B = ( Base ` W )
10		evlspw.i	\|- ( ph -> I e. V )
11		evlspw.s	\|- ( ph -> S e. CRing )
12		evlspw.r	\|- ( ph -> R e. ( SubRing ` S ) )
13		evlspw.n	\|- ( ph -> N e. NN0 )
14		evlspw.x	\|- ( ph -> X e. B )
15	1 2 5 6 8	evlsrhm	\|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom P ) )
16	10 11 12 15	syl3anc	\|- ( ph -> Q e. ( W RingHom P ) )
17	3 7	rhmmhm	\|- ( Q e. ( W RingHom P ) -> Q e. ( G MndHom H ) )
18	16 17	syl	\|- ( ph -> Q e. ( G MndHom H ) )
19	3 9	mgpbas	\|- B = ( Base ` G )
20		eqid	\|- ( .g ` H ) = ( .g ` H )
21	19 4 20	mhmmulg	\|- ( ( Q e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) )
22	18 13 14 21	syl3anc	\|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) )

Metamath Proof Explorer

Theorem evlspw

Proof