Metamath Proof Explorer


Theorem 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 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlspw.w 𝑊 = ( 𝐼 mPoly 𝑈 )
evlspw.g 𝐺 = ( mulGrp ‘ 𝑊 )
evlspw.e = ( .g𝐺 )
evlspw.u 𝑈 = ( 𝑆s 𝑅 )
evlspw.p 𝑃 = ( 𝑆s ( 𝐾m 𝐼 ) )
evlspw.h 𝐻 = ( mulGrp ‘ 𝑃 )
evlspw.k 𝐾 = ( Base ‘ 𝑆 )
evlspw.b 𝐵 = ( Base ‘ 𝑊 )
evlspw.i ( 𝜑𝐼𝑉 )
evlspw.s ( 𝜑𝑆 ∈ CRing )
evlspw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlspw.n ( 𝜑𝑁 ∈ ℕ0 )
evlspw.x ( 𝜑𝑋𝐵 )
Assertion evlspw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g𝐻 ) ( 𝑄𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlspw.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlspw.w 𝑊 = ( 𝐼 mPoly 𝑈 )
3 evlspw.g 𝐺 = ( mulGrp ‘ 𝑊 )
4 evlspw.e = ( .g𝐺 )
5 evlspw.u 𝑈 = ( 𝑆s 𝑅 )
6 evlspw.p 𝑃 = ( 𝑆s ( 𝐾m 𝐼 ) )
7 evlspw.h 𝐻 = ( mulGrp ‘ 𝑃 )
8 evlspw.k 𝐾 = ( Base ‘ 𝑆 )
9 evlspw.b 𝐵 = ( Base ‘ 𝑊 )
10 evlspw.i ( 𝜑𝐼𝑉 )
11 evlspw.s ( 𝜑𝑆 ∈ CRing )
12 evlspw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
13 evlspw.n ( 𝜑𝑁 ∈ ℕ0 )
14 evlspw.x ( 𝜑𝑋𝐵 )
15 1 2 5 6 8 evlsrhm ( ( 𝐼𝑉𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
16 10 11 12 15 syl3anc ( 𝜑𝑄 ∈ ( 𝑊 RingHom 𝑃 ) )
17 3 7 rhmmhm ( 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
18 16 17 syl ( 𝜑𝑄 ∈ ( 𝐺 MndHom 𝐻 ) )
19 3 9 mgpbas 𝐵 = ( Base ‘ 𝐺 )
20 eqid ( .g𝐻 ) = ( .g𝐻 )
21 19 4 20 mhmmulg ( ( 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0𝑋𝐵 ) → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g𝐻 ) ( 𝑄𝑋 ) ) )
22 18 13 14 21 syl3anc ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g𝐻 ) ( 𝑄𝑋 ) ) )