Theorem pwsvscaval

Description: Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsvscaval.y	|- Y = ( R ^s I )
	pwsvscaval.b	|- B = ( Base ` Y )
	pwsvscaval.s	|- .x. = ( .s ` R )
	pwsvscaval.t	|- .xb = ( .s ` Y )
	pwsvscaval.f	|- F = ( Scalar ` R )
	pwsvscaval.k	|- K = ( Base ` F )
	pwsvscaval.r	|- ( ph -> R e. V )
	pwsvscaval.i	|- ( ph -> I e. W )
	pwsvscaval.a	|- ( ph -> A e. K )
	pwsvscaval.x	|- ( ph -> X e. B )
	pwsvscaval.j	|- ( ph -> J e. I )
Assertion	pwsvscaval	|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwsvscaval.y	|- Y = ( R ^s I )
2		pwsvscaval.b	|- B = ( Base ` Y )
3		pwsvscaval.s	|- .x. = ( .s ` R )
4		pwsvscaval.t	|- .xb = ( .s ` Y )
5		pwsvscaval.f	|- F = ( Scalar ` R )
6		pwsvscaval.k	|- K = ( Base ` F )
7		pwsvscaval.r	|- ( ph -> R e. V )
8		pwsvscaval.i	|- ( ph -> I e. W )
9		pwsvscaval.a	|- ( ph -> A e. K )
10		pwsvscaval.x	|- ( ph -> X e. B )
11		pwsvscaval.j	|- ( ph -> J e. I )
12	1 2 3 4 5 6 7 8 9 10	pwsvscafval	|- ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )
13	12	fveq1d	|- ( ph -> ( ( A .xb X ) ` J ) = ( ( ( I X. { A } ) oF .x. X ) ` J ) )
14		eqid	|- ( Base ` R ) = ( Base ` R )
15	1 14 2 7 8 10	pwselbas	|- ( ph -> X : I --> ( Base ` R ) )
16	15	ffnd	|- ( ph -> X Fn I )
17		eqidd	|- ( ( ph /\ J e. I ) -> ( X ` J ) = ( X ` J ) )
18	8 9 16 17	ofc1	|- ( ( ph /\ J e. I ) -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( A .x. ( X ` J ) ) )
19	11 18	mpdan	|- ( ph -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( A .x. ( X ` J ) ) )
20	13 19	eqtrd	|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )