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 ⊢ Q = I evalSub R ⁡ S
evlscl.p ⊢ P = I mPoly U
evlscl.u ⊢ U = R ↾ 𝑠 S
evlscl.b ⊢ B = Base P
evlscl.k ⊢ K = Base R
evlscl.i ⊢ φ → I ∈ V
evlscl.r ⊢ φ → R ∈ CRing
evlscl.s ⊢ φ → S ∈ SubRing ⁡ R
evlscl.f ⊢ φ → F ∈ B
evlscl.a ⊢ φ → A ∈ K I
Assertion evlscl ⊢ φ → Q ⁡ F ⁡ A ∈ K

Proof

Step Hyp Ref Expression
1 evlscl.q ⊢ Q = I evalSub R ⁡ S
2 evlscl.p ⊢ P = I mPoly U
3 evlscl.u ⊢ U = R ↾ 𝑠 S
4 evlscl.b ⊢ B = Base P
5 evlscl.k ⊢ K = Base R
6 evlscl.i ⊢ φ → I ∈ V
7 evlscl.r ⊢ φ → R ∈ CRing
8 evlscl.s ⊢ φ → S ∈ SubRing ⁡ R
9 evlscl.f ⊢ φ → F ∈ B
10 evlscl.a ⊢ φ → A ∈ K I
11 eqid ⊢ R ↑ 𝑠 K I = R ↑ 𝑠 K I
12 eqid ⊢ Base R ↑ 𝑠 K I = Base R ↑ 𝑠 K I
13 ovexd ⊢ φ → K I ∈ V
14 1 2 3 11 5 evlsrhm ⊢ I ∈ V ∧ R ∈ CRing ∧ S ∈ SubRing ⁡ R → Q ∈ P RingHom R ↑ 𝑠 K I
15 6 7 8 14 syl3anc ⊢ φ → Q ∈ P RingHom R ↑ 𝑠 K I
16 4 12 rhmf ⊢ Q ∈ P RingHom R ↑ 𝑠 K I → Q : B ⟶ Base R ↑ 𝑠 K I
17 15 16 syl ⊢ φ → Q : B ⟶ Base R ↑ 𝑠 K I
18 17 9 ffvelcdmd ⊢ φ → Q ⁡ F ∈ Base R ↑ 𝑠 K I
19 11 5 12 7 13 18 pwselbas ⊢ φ → Q ⁡ F : K I ⟶ K
20 19 10 ffvelcdmd ⊢ φ → Q ⁡ F ⁡ A ∈ K