Theorem evlcl

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

	Ref	Expression
Hypotheses	evlcl.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evlcl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	evlcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlcl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	evlcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlcl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evlcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	evlcl.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlcl	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )

Proof

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