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

Metamath Proof Explorer

Theorem evlsca

Description: Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlsca.q ⊢ Q = I eval S
evlsca.w ⊢ W = I mPoly S
evlsca.b ⊢ B = Base S
evlsca.a ⊢ A = algSc ⁡ W
evlsca.i ⊢ φ → I ∈ V
evlsca.s ⊢ φ → S ∈ CRing
evlsca.x ⊢ φ → X ∈ B
Assertion evlsca ⊢ φ → Q ⁡ A ⁡ X = B I × X

Proof

Step Hyp Ref Expression
1 evlsca.q ⊢ Q = I eval S
2 evlsca.w ⊢ W = I mPoly S
3 evlsca.b ⊢ B = Base S
4 evlsca.a ⊢ A = algSc ⁡ W
5 evlsca.i ⊢ φ → I ∈ V
6 evlsca.s ⊢ φ → S ∈ CRing
7 evlsca.x ⊢ φ → X ∈ B
8 eqid ⊢ I evalSub S ⁡ B = I evalSub S ⁡ B
9 eqid ⊢ I mPoly S ↾ 𝑠 B = I mPoly S ↾ 𝑠 B
10 eqid ⊢ S ↾ 𝑠 B = S ↾ 𝑠 B
11 eqid ⊢ algSc ⁡ I mPoly S ↾ 𝑠 B = algSc ⁡ I mPoly S ↾ 𝑠 B
12 crngring ⊢ S ∈ CRing → S ∈ Ring
13 3 subrgid ⊢ S ∈ Ring → B ∈ SubRing ⁡ S
14 6 12 13 3syl ⊢ φ → B ∈ SubRing ⁡ S
15 8 1 9 10 2 3 11 4 5 6 14 7 evlsscasrng ⊢ φ → I evalSub S ⁡ B ⁡ algSc ⁡ I mPoly S ↾ 𝑠 B ⁡ X = Q ⁡ A ⁡ X
16 8 9 10 3 11 5 6 14 7 evlssca ⊢ φ → I evalSub S ⁡ B ⁡ algSc ⁡ I mPoly S ↾ 𝑠 B ⁡ X = B I × X
17 15 16 eqtr3d ⊢ φ → Q ⁡ A ⁡ X = B I × X