Metamath Proof Explorer


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=SevalSub1R
evls1pw.u U=S𝑠R
evls1pw.w W=Poly1U
evls1pw.g G=mulGrpW
evls1pw.k K=BaseS
evls1pw.b B=BaseW
evls1pw.e ×˙=G
evls1pw.s φSCRing
evls1pw.r φRSubRingS
evls1pw.n φN0
evls1pw.x φXB
Assertion evls1pw φQN×˙X=NmulGrpS𝑠KQX

Proof

Step Hyp Ref Expression
1 evls1pw.q Q=SevalSub1R
2 evls1pw.u U=S𝑠R
3 evls1pw.w W=Poly1U
4 evls1pw.g G=mulGrpW
5 evls1pw.k K=BaseS
6 evls1pw.b B=BaseW
7 evls1pw.e ×˙=G
8 evls1pw.s φSCRing
9 evls1pw.r φRSubRingS
10 evls1pw.n φN0
11 evls1pw.x φXB
12 eqid S𝑠K=S𝑠K
13 1 5 12 2 3 evls1rhm SCRingRSubRingSQWRingHomS𝑠K
14 8 9 13 syl2anc φQWRingHomS𝑠K
15 eqid mulGrpS𝑠K=mulGrpS𝑠K
16 4 15 rhmmhm QWRingHomS𝑠KQGMndHommulGrpS𝑠K
17 14 16 syl φQGMndHommulGrpS𝑠K
18 4 6 mgpbas B=BaseG
19 eqid mulGrpS𝑠K=mulGrpS𝑠K
20 18 7 19 mhmmulg QGMndHommulGrpS𝑠KN0XBQN×˙X=NmulGrpS𝑠KQX
21 17 10 11 20 syl3anc φQN×˙X=NmulGrpS𝑠KQX