Theorem mplvsca2

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplvsca2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplvsca2.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplvsca2.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
Assertion	mplvsca2	⊢ · = ( ·𝑠 ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mplvsca2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplvsca2.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3		mplvsca2.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
4		fvex	⊢ ( Base ‘ 𝑃 ) ∈ V
5		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6	1 2 5	mplval2	⊢ 𝑃 = ( 𝑆 ↾s ( Base ‘ 𝑃 ) )
7		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
8	6 7	ressvsca	⊢ ( ( Base ‘ 𝑃 ) ∈ V → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) )
9	4 8	ax-mp	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 )
10	3 9	eqtr4i	⊢ · = ( ·𝑠 ‘ 𝑆 )