Theorem psrvscaval

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 )
	psrvscaval.y	|- ( ph -> Y e. D )
Assertion	psrvscaval	|- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )

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		psrvscaval.y	|- ( ph -> Y e. D )
10	1 2 3 4 5 6 7 8	psrvsca	|- ( 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	1 3 6 4 8	psrelbas	|- ( ph -> F : D --> K )
16	15	ffnd	|- ( ph -> F Fn D )
17		eqidd	|- ( ( ph /\ Y e. D ) -> ( F ` Y ) = ( F ` Y ) )
18	14 7 16 17	ofc1	|- ( ( ph /\ Y e. D ) -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
19	9 18	mpdan	|- ( ph -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
20	11 19	eqtrd	|- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )