Theorem mplvsca

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

	Ref	Expression
Hypotheses	mplvsca.p	|- P = ( I mPoly R )
	mplvsca.n	|- .xb = ( .s ` P )
	mplvsca.k	|- K = ( Base ` R )
	mplvsca.b	|- B = ( Base ` P )
	mplvsca.m	|- .x. = ( .r ` R )
	mplvsca.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	mplvsca.x	|- ( ph -> X e. K )
	mplvsca.f	|- ( ph -> F e. B )
Assertion	mplvsca	|- ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )

Proof

Step	Hyp	Ref	Expression
1		mplvsca.p	|- P = ( I mPoly R )
2		mplvsca.n	|- .xb = ( .s ` P )
3		mplvsca.k	|- K = ( Base ` R )
4		mplvsca.b	|- B = ( Base ` P )
5		mplvsca.m	|- .x. = ( .r ` R )
6		mplvsca.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7		mplvsca.x	|- ( ph -> X e. K )
8		mplvsca.f	|- ( ph -> F e. B )
9		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
10	1 9 2	mplvsca2	|- .xb = ( .s ` ( I mPwSer R ) )
11		eqid	|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
12	1 9 4 11	mplbasss	|- B C_ ( Base ` ( I mPwSer R ) )
13	12 8	sselid	|- ( ph -> F e. ( Base ` ( I mPwSer R ) ) )
14	9 10 3 11 5 6 7 13	psrvsca	|- ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )