Metamath Proof Explorer

Theorem evlsvar

Description: Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsvar.q ⊢ Q = I evalSub S ⁡ R
evlsvar.v ⊢ V = I mVar U
evlsvar.u ⊢ U = S ↾ 𝑠 R
evlsvar.b ⊢ B = Base S
evlsvar.i ⊢ φ → I ∈ W
evlsvar.s ⊢ φ → S ∈ CRing
evlsvar.r ⊢ φ → R ∈ SubRing ⁡ S
evlsvar.x ⊢ φ → X ∈ I
Assertion evlsvar ⊢ φ → Q ⁡ V ⁡ X = g ∈ B I ⟼ g ⁡ X

Proof

Step Hyp Ref Expression
1 evlsvar.q ⊢ Q = I evalSub S ⁡ R
2 evlsvar.v ⊢ V = I mVar U
3 evlsvar.u ⊢ U = S ↾ 𝑠 R
4 evlsvar.b ⊢ B = Base S
5 evlsvar.i ⊢ φ → I ∈ W
6 evlsvar.s ⊢ φ → S ∈ CRing
7 evlsvar.r ⊢ φ → R ∈ SubRing ⁡ S
8 evlsvar.x ⊢ φ → X ∈ I
9 eqid ⊢ I mPoly U = I mPoly U
10 eqid ⊢ S ↑ 𝑠 B I = S ↑ 𝑠 B I
11 eqid ⊢ algSc ⁡ I mPoly U = algSc ⁡ I mPoly U
12 eqid ⊢ x ∈ R ⟼ B I × x = x ∈ R ⟼ B I × x
13 eqid ⊢ x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
14 1 9 2 3 10 4 11 12 13 evlsval2 ⊢ I ∈ W ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q ∈ I mPoly U RingHom S ↑ 𝑠 B I ∧ Q ∘ algSc ⁡ I mPoly U = x ∈ R ⟼ B I × x ∧ Q ∘ V = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
15 5 6 7 14 syl3anc ⊢ φ → Q ∈ I mPoly U RingHom S ↑ 𝑠 B I ∧ Q ∘ algSc ⁡ I mPoly U = x ∈ R ⟼ B I × x ∧ Q ∘ V = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
16 15 simprrd ⊢ φ → Q ∘ V = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
17 16 fveq1d ⊢ φ → Q ∘ V ⁡ X = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x ⁡ X
18 eqid ⊢ Base I mPoly U = Base I mPoly U
19 3 subrgring ⊢ R ∈ SubRing ⁡ S → U ∈ Ring
20 7 19 syl ⊢ φ → U ∈ Ring
21 9 2 18 5 20 mvrf2 ⊢ φ → V : I ⟶ Base I mPoly U
22 21 ffnd ⊢ φ → V Fn I
23 fvco2 ⊢ V Fn I ∧ X ∈ I → Q ∘ V ⁡ X = Q ⁡ V ⁡ X
24 22 8 23 syl2anc ⊢ φ → Q ∘ V ⁡ X = Q ⁡ V ⁡ X
25 fveq2 ⊢ x = X → g ⁡ x = g ⁡ X
26 25 mpteq2dv ⊢ x = X → g ∈ B I ⟼ g ⁡ x = g ∈ B I ⟼ g ⁡ X
27 ovex ⊢ B I ∈ V
28 27 mptex ⊢ g ∈ B I ⟼ g ⁡ X ∈ V
29 26 13 28 fvmpt ⊢ X ∈ I → x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x ⁡ X = g ∈ B I ⟼ g ⁡ X
30 8 29 syl ⊢ φ → x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x ⁡ X = g ∈ B I ⟼ g ⁡ X
31 17 24 30 3eqtr3d ⊢ φ → Q ⁡ V ⁡ X = g ∈ B I ⟼ g ⁡ X