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

Metamath Proof Explorer

Theorem evlvarval

Description: Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlvarval.1 ⊢ Q = I eval S
evlvarval.2 ⊢ P = I mPoly S
evlvarval.3 ⊢ K = Base S
evlvarval.4 ⊢ B = Base P
evlvarval.5 ⊢ ∙ ˙ = ⋅ P
evlvarval.6 ⊢ · ˙ = ⋅ S
evlvarval.7 ⊢ φ → I ∈ Z
evlvarval.8 ⊢ φ → S ∈ CRing
evlvarval.9 ⊢ φ → A ∈ K I
evlvarval.10 ⊢ V = I mVar S
evlvarval.11 ⊢ φ → X ∈ I
Assertion evlvarval ⊢ φ → V ⁡ X ∈ B ∧ Q ⁡ V ⁡ X ⁡ A = A ⁡ X

Proof

Step Hyp Ref Expression
1 evlvarval.1 ⊢ Q = I eval S
2 evlvarval.2 ⊢ P = I mPoly S
3 evlvarval.3 ⊢ K = Base S
4 evlvarval.4 ⊢ B = Base P
5 evlvarval.5 ⊢ ∙ ˙ = ⋅ P
6 evlvarval.6 ⊢ · ˙ = ⋅ S
7 evlvarval.7 ⊢ φ → I ∈ Z
8 evlvarval.8 ⊢ φ → S ∈ CRing
9 evlvarval.9 ⊢ φ → A ∈ K I
10 evlvarval.10 ⊢ V = I mVar S
11 evlvarval.11 ⊢ φ → X ∈ I
12 8 crngringd ⊢ φ → S ∈ Ring
13 2 10 4 7 12 11 mvrcl ⊢ φ → V ⁡ X ∈ B
14 fveq1 ⊢ a = A → a ⁡ X = A ⁡ X
15 1 10 3 7 8 11 evlvar ⊢ φ → Q ⁡ V ⁡ X = a ∈ K I ⟼ a ⁡ X
16 3 fvexi ⊢ K ∈ V
17 16 a1i ⊢ φ → K ∈ V
18 7 17 9 elmaprd ⊢ φ → A : I ⟶ K
19 18 11 ffvelcdmd ⊢ φ → A ⁡ X ∈ K
20 14 15 9 19 fvmptd4 ⊢ φ → Q ⁡ V ⁡ X ⁡ A = A ⁡ X
21 13 20 jca ⊢ φ → V ⁡ X ∈ B ∧ Q ⁡ V ⁡ X ⁡ A = A ⁡ X