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 
|- ( ph -> I e. V )
mplsca.r 
|- ( ph -> R e. W )
Assertion mplsca 
|- ( ph -> R = ( Scalar ` P ) )

Proof

Step Hyp Ref Expression
1 mplsca.p 
 |-  P = ( I mPoly R )
2 mplsca.i 
 |-  ( ph -> I e. V )
3 mplsca.r 
 |-  ( ph -> R e. W )
4 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
5 4 2 3 psrsca 
 |-  ( ph -> R = ( Scalar ` ( I mPwSer R ) ) )
6 fvex 
 |-  ( Base ` P ) e. _V
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 1 4 7 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
9 eqid 
 |-  ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` ( I mPwSer R ) )
10 8 9 resssca 
 |-  ( ( Base ` P ) e. _V -> ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` P ) )
11 6 10 ax-mp 
 |-  ( Scalar ` ( I mPwSer R ) ) = ( Scalar ` P )
12 5 11 eqtrdi 
 |-  ( ph -> R = ( Scalar ` P ) )