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

Metamath Proof Explorer

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 ⊢ Q = I eval R
evlcl.p ⊢ P = I mPoly R
evlcl.b ⊢ B = Base P
evlcl.k ⊢ K = Base R
evlcl.i ⊢ φ → I ∈ V
evlcl.r ⊢ φ → R ∈ CRing
evlcl.f ⊢ φ → F ∈ B
evlcl.a ⊢ φ → A ∈ K I
Assertion evlcl ⊢ φ → Q ⁡ F ⁡ A ∈ K

Proof

Step Hyp Ref Expression
1 evlcl.q ⊢ Q = I eval R
2 evlcl.p ⊢ P = I mPoly R
3 evlcl.b ⊢ B = Base P
4 evlcl.k ⊢ K = Base R
5 evlcl.i ⊢ φ → I ∈ V
6 evlcl.r ⊢ φ → R ∈ CRing
7 evlcl.f ⊢ φ → F ∈ B
8 evlcl.a ⊢ φ → A ∈ K I
9 eqid ⊢ R ↑ 𝑠 K I = R ↑ 𝑠 K I
10 eqid ⊢ Base R ↑ 𝑠 K I = Base R ↑ 𝑠 K I
11 ovexd ⊢ φ → K I ∈ V
12 1 4 2 9 evlrhm ⊢ I ∈ V ∧ R ∈ CRing → Q ∈ P RingHom R ↑ 𝑠 K I
13 5 6 12 syl2anc ⊢ φ → Q ∈ P RingHom R ↑ 𝑠 K I
14 3 10 rhmf ⊢ Q ∈ P RingHom R ↑ 𝑠 K I → Q : B ⟶ Base R ↑ 𝑠 K I
15 13 14 syl ⊢ φ → Q : B ⟶ Base R ↑ 𝑠 K I
16 15 7 ffvelcdmd ⊢ φ → Q ⁡ F ∈ Base R ↑ 𝑠 K I
17 9 4 10 6 11 16 pwselbas ⊢ φ → Q ⁡ F : K I ⟶ K
18 17 8 ffvelcdmd ⊢ φ → Q ⁡ F ⁡ A ∈ K