Theorem psrvsca

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		psrvsca.s	|- S = ( I mPwSer R )
2		psrvsca.n	|- .xb = ( .s ` S )
3		psrvsca.k	|- K = ( Base ` R )
4		psrvsca.b	|- B = ( Base ` S )
5		psrvsca.m	|- .x. = ( .r ` R )
6		psrvsca.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7		psrvsca.x	|- ( ph -> X e. K )
8		psrvsca.y	|- ( ph -> F e. B )
9		sneq	|- ( x = X -> { x } = { X } )
10	9	xpeq2d	|- ( x = X -> ( D X. { x } ) = ( D X. { X } ) )
11	10	oveq1d	|- ( x = X -> ( ( D X. { x } ) oF .x. f ) = ( ( D X. { X } ) oF .x. f ) )
12		oveq2	|- ( f = F -> ( ( D X. { X } ) oF .x. f ) = ( ( D X. { X } ) oF .x. F ) )
13	1 2 3 4 5 6	psrvscafval	|- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
14		ovex	|- ( ( D X. { X } ) oF .x. F ) e. _V
15	11 12 13 14	ovmpo	|- ( ( X e. K /\ F e. B ) -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )
16	7 8 15	syl2anc	|- ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )