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