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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplsca.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplsca.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion mplsca ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 mplsca.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplsca.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 mplsca.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
5 4 2 3 psrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) )
6 fvex ⊢ ( Base ‘ 𝑃 ) ∈ V
7 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 1 4 7 mplval2 ⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
9 eqid ⊢ ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) )
10 8 9 resssca ⊢ ( ( Base ‘ 𝑃 ) ∈ V → ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Scalar ‘ 𝑃 ) )
11 6 10 ax-mp ⊢ ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Scalar ‘ 𝑃 )
12 5 11 eqtrdi ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )