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

Metamath Proof Explorer

Theorem fveval1fvcl

Description: The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019)

Ref Expression
Hypotheses fveval1fvcl.q ⊢ O = eval 1 ⁡ R
fveval1fvcl.p ⊢ P = Poly 1 ⁡ R
fveval1fvcl.b ⊢ B = Base R
fveval1fvcl.u ⊢ U = Base P
fveval1fvcl.r ⊢ φ → R ∈ CRing
fveval1fvcl.y ⊢ φ → Y ∈ B
fveval1fvcl.m ⊢ φ → M ∈ U
Assertion fveval1fvcl ⊢ φ → O ⁡ M ⁡ Y ∈ B

Proof

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