Theorem evlscl

Description: A polynomial over the ring R evaluates to an element in R . (Contributed by SN, 12-Mar-2025)

	Ref	Expression
Hypotheses	evlscl.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝑆 )
	evlscl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlscl.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
	evlscl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	evlscl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlscl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evlscl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	evlscl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	evlscl.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlscl	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		evlscl.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝑆 )
2		evlscl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlscl.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
4		evlscl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		evlscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
6		evlscl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		evlscl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
8		evlscl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
9		evlscl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		evlscl.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
11		eqid	⊢ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) )
12		eqid	⊢ ( Base ‘ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) )
13		ovexd	⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
14	1 2 3 11 5	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
15	6 7 8 14	syl3anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
16	4 12	rhmf	⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
17	15 16	syl	⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
18	17 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
19	11 5 12 7 13 18	pwselbas	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
20	19 10	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )