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\mathrm{mPoly}R$$
	mplsca.i	$$⊢\phi \to I\in V$$
	mplsca.r	$$⊢\phi \to R\in W$$
Assertion	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplsca.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplsca.i	$$⊢\phi \to I\in V$$
3		mplsca.r	$$⊢\phi \to R\in W$$
4		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
5	4 2 3	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)$$
6		fvex	$$⊢{\mathrm{Base}}_P\in \mathrm{V}$$
7		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
8	1 4 7	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_P$$
9		eqid	$$⊢\mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)=\mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)$$
10	8 9	resssca	$$⊢{\mathrm{Base}}_P\in \mathrm{V}\to \mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)=\mathrm{Scalar}\left(P\right)$$
11	6 10	ax-mp	$$⊢\mathrm{Scalar}\left(I\mathrm{mPwSer}R\right)=\mathrm{Scalar}\left(P\right)$$
12	5 11	eqtrdi	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$