Theorem evls1varpw

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

	Ref	Expression
Hypotheses	evls1varpw.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1varpw.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1varpw.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	evls1varpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
	evls1varpw.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
	evls1varpw.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1varpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
	evls1varpw.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1varpw.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1varpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	evls1varpw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evls1varpw.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1varpw.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3		evls1varpw.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4		evls1varpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
5		evls1varpw.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
6		evls1varpw.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		evls1varpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
8		evls1varpw.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evls1varpw.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evls1varpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12	2	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
13	5 3 11	vr1cl	⊢ ( 𝑈 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
14	9 12 13	3syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15	1 2 3 4 6 11 7 8 9 10 14	evls1pw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )