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