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

Metamath Proof Explorer

Theorem evls1scafv

Description: Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025)

Ref Expression
Hypotheses evls1scafv.q ⊢ Q = S evalSub 1 R
evls1scafv.w ⊢ W = Poly 1 ⁡ U
evls1scafv.u ⊢ U = S ↾ 𝑠 R
evls1scafv.b ⊢ B = Base S
evls1scafv.a ⊢ A = algSc ⁡ W
evls1scafv.s ⊢ φ → S ∈ CRing
evls1scafv.r ⊢ φ → R ∈ SubRing ⁡ S
evls1scafv.x ⊢ φ → X ∈ R
evls1scafv.1 ⊢ φ → C ∈ B
Assertion evls1scafv ⊢ φ → Q ⁡ A ⁡ X ⁡ C = X

Proof

Step Hyp Ref Expression
1 evls1scafv.q ⊢ Q = S evalSub 1 R
2 evls1scafv.w ⊢ W = Poly 1 ⁡ U
3 evls1scafv.u ⊢ U = S ↾ 𝑠 R
4 evls1scafv.b ⊢ B = Base S
5 evls1scafv.a ⊢ A = algSc ⁡ W
6 evls1scafv.s ⊢ φ → S ∈ CRing
7 evls1scafv.r ⊢ φ → R ∈ SubRing ⁡ S
8 evls1scafv.x ⊢ φ → X ∈ R
9 evls1scafv.1 ⊢ φ → C ∈ B
10 1 2 3 4 5 6 7 8 evls1sca ⊢ φ → Q ⁡ A ⁡ X = B × X
11 10 fveq1d ⊢ φ → Q ⁡ A ⁡ X ⁡ C = B × X ⁡ C
12 fvconst2g ⊢ X ∈ R ∧ C ∈ B → B × X ⁡ C = X
13 8 9 12 syl2anc ⊢ φ → B × X ⁡ C = X
14 11 13 eqtrd ⊢ φ → Q ⁡ A ⁡ X ⁡ C = X