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

Metamath Proof Explorer

Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsvarval.q ⊢ Q = I evalSub S ⁡ R
evlsvarval.p ⊢ P = I mPoly U
evlsvarval.v ⊢ V = I mVar U
evlsvarval.u ⊢ U = S ↾ 𝑠 R
evlsvarval.k ⊢ K = Base S
evlsvarval.b ⊢ B = Base P
evlsvarval.i ⊢ φ → I ∈ W
evlsvarval.s ⊢ φ → S ∈ CRing
evlsvarval.r ⊢ φ → R ∈ SubRing ⁡ S
evlsvarval.x ⊢ φ → X ∈ I
evlsvarval.a ⊢ φ → A ∈ K I
Assertion evlsvarval ⊢ φ → V ⁡ X ∈ B ∧ Q ⁡ V ⁡ X ⁡ A = A ⁡ X

Proof

Step Hyp Ref Expression
1 evlsvarval.q ⊢ Q = I evalSub S ⁡ R
2 evlsvarval.p ⊢ P = I mPoly U
3 evlsvarval.v ⊢ V = I mVar U
4 evlsvarval.u ⊢ U = S ↾ 𝑠 R
5 evlsvarval.k ⊢ K = Base S
6 evlsvarval.b ⊢ B = Base P
7 evlsvarval.i ⊢ φ → I ∈ W
8 evlsvarval.s ⊢ φ → S ∈ CRing
9 evlsvarval.r ⊢ φ → R ∈ SubRing ⁡ S
10 evlsvarval.x ⊢ φ → X ∈ I
11 evlsvarval.a ⊢ φ → A ∈ K I
12 4 subrgring ⊢ R ∈ SubRing ⁡ S → U ∈ Ring
13 9 12 syl ⊢ φ → U ∈ Ring
14 2 3 6 7 13 10 mvrcl ⊢ φ → V ⁡ X ∈ B
15 fveq1 ⊢ g = A → g ⁡ X = A ⁡ X
16 1 3 4 5 7 8 9 10 evlsvar ⊢ φ → Q ⁡ V ⁡ X = g ∈ K I ⟼ g ⁡ X
17 fvexd ⊢ φ → A ⁡ X ∈ V
18 15 16 11 17 fvmptd4 ⊢ φ → Q ⁡ V ⁡ X ⁡ A = A ⁡ X
19 14 18 jca ⊢ φ → V ⁡ X ∈ B ∧ Q ⁡ V ⁡ X ⁡ A = A ⁡ X