This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )