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

Metamath Proof Explorer

Theorem mplsca

Description: The scalar field of a multivariate polynomial structure. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplsca.p ⊢ P = I mPoly R
mplsca.i ⊢ φ → I ∈ V
mplsca.r ⊢ φ → R ∈ W
Assertion mplsca ⊢ φ → R = Scalar ⁡ P

Proof

Step Hyp Ref Expression
1 mplsca.p ⊢ P = I mPoly R
2 mplsca.i ⊢ φ → I ∈ V
3 mplsca.r ⊢ φ → R ∈ W
4 eqid ⊢ I mPwSer R = I mPwSer R
5 4 2 3 psrsca ⊢ φ → R = Scalar ⁡ I mPwSer R
6 fvex ⊢ Base P ∈ V
7 eqid ⊢ Base P = Base P
8 1 4 7 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
9 eqid ⊢ Scalar ⁡ I mPwSer R = Scalar ⁡ I mPwSer R
10 8 9 resssca ⊢ Base P ∈ V → Scalar ⁡ I mPwSer R = Scalar ⁡ P
11 6 10 ax-mp ⊢ Scalar ⁡ I mPwSer R = Scalar ⁡ P
12 5 11 eqtrdi ⊢ φ → R = Scalar ⁡ P