# 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 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1pw.u 𝑈 = ( 𝑆s 𝑅 )
evls1pw.w 𝑊 = ( Poly1𝑈 )
evls1pw.g 𝐺 = ( mulGrp ‘ 𝑊 )
evls1pw.k 𝐾 = ( Base ‘ 𝑆 )
evls1pw.b 𝐵 = ( Base ‘ 𝑊 )
evls1pw.e = ( .g𝐺 )
evls1pw.s ( 𝜑𝑆 ∈ CRing )
evls1pw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1pw.n ( 𝜑𝑁 ∈ ℕ0 )
evls1pw.x ( 𝜑𝑋𝐵 )
Assertion evls1pw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) ( 𝑄𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 evls1pw.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1pw.u 𝑈 = ( 𝑆s 𝑅 )
3 evls1pw.w 𝑊 = ( Poly1𝑈 )
4 evls1pw.g 𝐺 = ( mulGrp ‘ 𝑊 )
5 evls1pw.k 𝐾 = ( Base ‘ 𝑆 )
6 evls1pw.b 𝐵 = ( Base ‘ 𝑊 )
7 evls1pw.e = ( .g𝐺 )
8 evls1pw.s ( 𝜑𝑆 ∈ CRing )
9 evls1pw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evls1pw.n ( 𝜑𝑁 ∈ ℕ0 )
11 evls1pw.x ( 𝜑𝑋𝐵 )
12 eqid ( 𝑆s 𝐾 ) = ( 𝑆s 𝐾 )
13 1 5 12 2 3 evls1rhm ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆s 𝐾 ) ) )
14 8 9 13 syl2anc ( 𝜑𝑄 ∈ ( 𝑊 RingHom ( 𝑆s 𝐾 ) ) )
15 eqid ( mulGrp ‘ ( 𝑆s 𝐾 ) ) = ( mulGrp ‘ ( 𝑆s 𝐾 ) )
16 4 15 rhmmhm ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆s 𝐾 ) ) → 𝑄 ∈ ( 𝐺 MndHom ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) )
17 14 16 syl ( 𝜑𝑄 ∈ ( 𝐺 MndHom ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) )
18 4 6 mgpbas 𝐵 = ( Base ‘ 𝐺 )
19 eqid ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐾 ) ) )
20 18 7 19 mhmmulg ( ( 𝑄 ∈ ( 𝐺 MndHom ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) ∧ 𝑁 ∈ ℕ0𝑋𝐵 ) → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) ( 𝑄𝑋 ) ) )
21 17 10 11 20 syl3anc ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐾 ) ) ) ( 𝑄𝑋 ) ) )