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