Theorem prdsvscaval

Description: Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	|- Y = ( S Xs_ R )
	prdsbasmpt.b	|- B = ( Base ` Y )
	prdsvscaval.t	|- .x. = ( .s ` Y )
	prdsvscaval.k	|- K = ( Base ` S )
	prdsvscaval.s	|- ( ph -> S e. V )
	prdsvscaval.i	|- ( ph -> I e. W )
	prdsvscaval.r	|- ( ph -> R Fn I )
	prdsvscaval.f	|- ( ph -> F e. K )
	prdsvscaval.g	|- ( ph -> G e. B )
Assertion	prdsvscaval	|- ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	|- Y = ( S Xs_ R )
2		prdsbasmpt.b	|- B = ( Base ` Y )
3		prdsvscaval.t	|- .x. = ( .s ` Y )
4		prdsvscaval.k	|- K = ( Base ` S )
5		prdsvscaval.s	|- ( ph -> S e. V )
6		prdsvscaval.i	|- ( ph -> I e. W )
7		prdsvscaval.r	|- ( ph -> R Fn I )
8		prdsvscaval.f	|- ( ph -> F e. K )
9		prdsvscaval.g	|- ( ph -> G e. B )
10		fnex	|- ( ( R Fn I /\ I e. W ) -> R e. _V )
11	7 6 10	syl2anc	|- ( ph -> R e. _V )
12	7	fndmd	|- ( ph -> dom R = I )
13	1 5 11 2 12 4 3	prdsvsca	|- ( ph -> .x. = ( y e. K , z e. B |-> ( x e. I |-> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) ) ) )
14		id	|- ( y = F -> y = F )
15		fveq1	|- ( z = G -> ( z ` x ) = ( G ` x ) )
16	14 15	oveqan12d	|- ( ( y = F /\ z = G ) -> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) = ( F ( .s ` ( R ` x ) ) ( G ` x ) ) )
17	16	adantl	|- ( ( ph /\ ( y = F /\ z = G ) ) -> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) = ( F ( .s ` ( R ` x ) ) ( G ` x ) ) )
18	17	mpteq2dv	|- ( ( ph /\ ( y = F /\ z = G ) ) -> ( x e. I |-> ( y ( .s ` ( R ` x ) ) ( z ` x ) ) ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )
19	6	mptexd	|- ( ph -> ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) e. _V )
20	13 18 8 9 19	ovmpod	|- ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )