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 ) )