Theorem prdsvscafval

Description: Scalar multiplication of a single coordinate in a structure product. (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 )
	prdsvscafval.j	|- ( ph -> J e. I )
Assertion	prdsvscafval	|- ( ph -> ( ( F .x. G ) ` J ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )

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		prdsvscafval.j	|- ( ph -> J e. I )
11	1 2 3 4 5 6 7 8 9	prdsvscaval	|- ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )
12		2fveq3	|- ( x = J -> ( .s ` ( R ` x ) ) = ( .s ` ( R ` J ) ) )
13		eqidd	|- ( x = J -> F = F )
14		fveq2	|- ( x = J -> ( G ` x ) = ( G ` J ) )
15	12 13 14	oveq123d	|- ( x = J -> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )
16	15	adantl	|- ( ( ph /\ x = J ) -> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )
17		ovexd	|- ( ph -> ( F ( .s ` ( R ` J ) ) ( G ` J ) ) e. _V )
18	11 16 10 17	fvmptd	|- ( ph -> ( ( F .x. G ) ` J ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )