Theorem evlsvarpw

Description: Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024)

	Ref	Expression
Hypotheses	evlsvarpw.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsvarpw.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
	evlsvarpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
	evlsvarpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
	evlsvarpw.x	⊢ 𝑋 = ( ( 𝐼 mVar 𝑈 ) ‘ 𝑌 )
	evlsvarpw.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvarpw.p	⊢ 𝑃 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
	evlsvarpw.h	⊢ 𝐻 = ( mulGrp ‘ 𝑃 )
	evlsvarpw.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlsvarpw.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsvarpw.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
	evlsvarpw.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvarpw.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvarpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	evlsvarpw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ 𝐻 ) ( 𝑄 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvarpw.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvarpw.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3		evlsvarpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
4		evlsvarpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
5		evlsvarpw.x	⊢ 𝑋 = ( ( 𝐼 mVar 𝑈 ) ‘ 𝑌 )
6		evlsvarpw.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
7		evlsvarpw.p	⊢ 𝑃 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
8		evlsvarpw.h	⊢ 𝐻 = ( mulGrp ‘ 𝑃 )
9		evlsvarpw.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
10		evlsvarpw.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		evlsvarpw.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
12		evlsvarpw.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
13		evlsvarpw.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
14		evlsvarpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16		eqid	⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 )
17	6	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
18	13 17	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
19	2 16 15 10 18 11	mvrcl	⊢ ( 𝜑 → ( ( 𝐼 mVar 𝑈 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
20	5 19	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
21	1 2 3 4 6 7 8 9 15 10 12 13 14 20	evlspw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ 𝐻 ) ( 𝑄 ‘ 𝑋 ) ) )