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