This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐾 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )