Theorem evls1varpwval

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		evls1varpwval.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1varpwval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3		evls1varpwval.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4		evls1varpwval.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
5		evls1varpwval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
6		evls1varpwval.e	⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
7		evls1varpwval.f	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
8		evls1varpwval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evls1varpwval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evls1varpwval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		evls1varpwval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
12		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13	2	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
14	4 3 12	vr1cl	⊢ ( 𝑈 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15	9 13 14	3syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
16	1 5 3 2 12 8 9 6 7 10 15 11	evls1expd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) ) )
17	1 4 2 5 8 9	evls1var	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) = ( ( I ↾ 𝐵 ) ‘ 𝐶 ) )
19		fvresi	⊢ ( 𝐶 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝐶 ) = 𝐶 )
20	11 19	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐵 ) ‘ 𝐶 ) = 𝐶 )
21	18 20	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) = 𝐶 )
22	21	oveq2d	⊢ ( 𝜑 → ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) ) = ( 𝑁 ↑ 𝐶 ) )
23	16 22	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ 𝐶 ) )