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

Metamath Proof Explorer

Theorem evl1fvf

Description: The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses evl1fvf.o ⊢ O = eval 1 ⁡ R
evl1fvf.p ⊢ P = Poly 1 ⁡ R
evl1fvf.u ⊢ U = Base P
evl1fvf.r ⊢ φ → R ∈ CRing
evl1fvf.b ⊢ B = Base R
evl1fvf.q ⊢ φ → Q ∈ U
Assertion evl1fvf ⊢ φ → O ⁡ Q : B ⟶ B

Proof

Step Hyp Ref Expression
1 evl1fvf.o ⊢ O = eval 1 ⁡ R
2 evl1fvf.p ⊢ P = Poly 1 ⁡ R
3 evl1fvf.u ⊢ U = Base P
4 evl1fvf.r ⊢ φ → R ∈ CRing
5 evl1fvf.b ⊢ B = Base R
6 evl1fvf.q ⊢ φ → Q ∈ U
7 eqid ⊢ R ↑ 𝑠 B = R ↑ 𝑠 B
8 eqid ⊢ Base R ↑ 𝑠 B = Base R ↑ 𝑠 B
9 5 fvexi ⊢ B ∈ V
10 9 a1i ⊢ φ → B ∈ V
11 1 2 7 5 evl1rhm ⊢ R ∈ CRing → O ∈ P RingHom R ↑ 𝑠 B
12 3 8 rhmf ⊢ O ∈ P RingHom R ↑ 𝑠 B → O : U ⟶ Base R ↑ 𝑠 B
13 4 11 12 3syl ⊢ φ → O : U ⟶ Base R ↑ 𝑠 B
14 13 6 ffvelcdmd ⊢ φ → O ⁡ Q ∈ Base R ↑ 𝑠 B
15 7 5 8 4 10 14 pwselbas ⊢ φ → O ⁡ Q : B ⟶ B