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 ) ) )

Metamath Proof Explorer

Theorem evls1pw

Proof