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 evalSub1 R )
	evls1pw.u	|- U = ( S |`s R )
	evls1pw.w	|- W = ( Poly1 ` U )
	evls1pw.g	|- G = ( mulGrp ` W )
	evls1pw.k	|- K = ( Base ` S )
	evls1pw.b	|- B = ( Base ` W )
	evls1pw.e	|- .^ = ( .g ` G )
	evls1pw.s	|- ( ph -> S e. CRing )
	evls1pw.r	|- ( ph -> R e. ( SubRing ` S ) )
	evls1pw.n	|- ( ph -> N e. NN0 )
	evls1pw.x	|- ( ph -> X e. B )
Assertion	evls1pw	|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		evls1pw.q	|- Q = ( S evalSub1 R )
2		evls1pw.u	|- U = ( S |`s R )
3		evls1pw.w	|- W = ( Poly1 ` U )
4		evls1pw.g	|- G = ( mulGrp ` W )
5		evls1pw.k	|- K = ( Base ` S )
6		evls1pw.b	|- B = ( Base ` W )
7		evls1pw.e	|- .^ = ( .g ` G )
8		evls1pw.s	|- ( ph -> S e. CRing )
9		evls1pw.r	|- ( ph -> R e. ( SubRing ` S ) )
10		evls1pw.n	|- ( ph -> N e. NN0 )
11		evls1pw.x	|- ( ph -> X e. B )
12		eqid	|- ( S ^s K ) = ( S ^s K )
13	1 5 12 2 3	evls1rhm	|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
14	8 9 13	syl2anc	|- ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
15		eqid	|- ( mulGrp ` ( S ^s K ) ) = ( mulGrp ` ( S ^s K ) )
16	4 15	rhmmhm	|- ( Q e. ( W RingHom ( S ^s K ) ) -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) )
17	14 16	syl	|- ( ph -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) )
18	4 6	mgpbas	|- B = ( Base ` G )
19		eqid	|- ( .g ` ( mulGrp ` ( S ^s K ) ) ) = ( .g ` ( mulGrp ` ( S ^s K ) ) )
20	18 7 19	mhmmulg	|- ( ( Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) /\ N e. NN0 /\ X e. B ) -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )
21	17 10 11 20	syl3anc	|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )