Theorem mplvscaval

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-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 )
	mplvscaval.y	|- ( ph -> Y e. D )
Assertion	mplvscaval	|- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )

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		mplvscaval.y	|- ( ph -> Y e. D )
10	1 2 3 4 5 6 7 8	mplvsca	|- ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )
11	10	fveq1d	|- ( ph -> ( ( X .xb F ) ` Y ) = ( ( ( D X. { X } ) oF .x. F ) ` Y ) )
12		ovex	|- ( NN0 ^m I ) e. _V
13	6 12	rabex2	|- D e. _V
14	13	a1i	|- ( ph -> D e. _V )
15		eqid	|- ( Base ` R ) = ( Base ` R )
16	1 15 4 6 8	mplelf	|- ( ph -> F : D --> ( Base ` R ) )
17	16	ffnd	|- ( ph -> F Fn D )
18		eqidd	|- ( ( ph /\ Y e. D ) -> ( F ` Y ) = ( F ` Y ) )
19	14 7 17 18	ofc1	|- ( ( ph /\ Y e. D ) -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
20	9 19	mpdan	|- ( ph -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
21	11 20	eqtrd	|- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )