Metamath Proof Explorer

Theorem evlvar

Description: Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlvar.q ⊢ Q = I eval S
evlvar.v ⊢ V = I mVar S
evlvar.b ⊢ B = Base S
evlvar.i ⊢ φ → I ∈ W
evlvar.s ⊢ φ → S ∈ CRing
evlvar.x ⊢ φ → X ∈ I
Assertion evlvar ⊢ φ → Q ⁡ V ⁡ X = g ∈ B I ⟼ g ⁡ X

Proof

Step Hyp Ref Expression
1 evlvar.q ⊢ Q = I eval S
2 evlvar.v ⊢ V = I mVar S
3 evlvar.b ⊢ B = Base S
4 evlvar.i ⊢ φ → I ∈ W
5 evlvar.s ⊢ φ → S ∈ CRing
6 evlvar.x ⊢ φ → X ∈ I
7 eqid ⊢ I evalSub S ⁡ B = I evalSub S ⁡ B
8 eqid ⊢ I mVar S ↾ 𝑠 B = I mVar S ↾ 𝑠 B
9 eqid ⊢ S ↾ 𝑠 B = S ↾ 𝑠 B
10 crngring ⊢ S ∈ CRing → S ∈ Ring
11 3 subrgid ⊢ S ∈ Ring → B ∈ SubRing ⁡ S
12 5 10 11 3syl ⊢ φ → B ∈ SubRing ⁡ S
13 7 1 8 9 3 4 5 12 6 evlsvarsrng ⊢ φ → I evalSub S ⁡ B ⁡ I mVar S ↾ 𝑠 B ⁡ X = Q ⁡ I mVar S ↾ 𝑠 B ⁡ X
14 7 8 9 3 4 5 12 6 evlsvar ⊢ φ → I evalSub S ⁡ B ⁡ I mVar S ↾ 𝑠 B ⁡ X = g ∈ B I ⟼ g ⁡ X
15 2 4 12 9 subrgmvr ⊢ φ → V = I mVar S ↾ 𝑠 B
16 15 fveq1d ⊢ φ → V ⁡ X = I mVar S ↾ 𝑠 B ⁡ X
17 16 eqcomd ⊢ φ → I mVar S ↾ 𝑠 B ⁡ X = V ⁡ X
18 17 fveq2d ⊢ φ → Q ⁡ I mVar S ↾ 𝑠 B ⁡ X = Q ⁡ V ⁡ X
19 13 14 18 3eqtr3rd ⊢ φ → Q ⁡ V ⁡ X = g ∈ B I ⟼ g ⁡ X