Theorem frlmvscaval

Description: Coordinates of a scalar multiple with respect to a basis in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	frlmvscaval.y	|- Y = ( R freeLMod I )
	frlmvscaval.b	|- B = ( Base ` Y )
	frlmvscaval.k	|- K = ( Base ` R )
	frlmvscaval.i	|- ( ph -> I e. W )
	frlmvscaval.a	|- ( ph -> A e. K )
	frlmvscaval.x	|- ( ph -> X e. B )
	frlmvscaval.j	|- ( ph -> J e. I )
	frlmvscaval.v	|- .xb = ( .s ` Y )
	frlmvscaval.t	|- .x. = ( .r ` R )
Assertion	frlmvscaval	|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmvscaval.y	|- Y = ( R freeLMod I )
2		frlmvscaval.b	|- B = ( Base ` Y )
3		frlmvscaval.k	|- K = ( Base ` R )
4		frlmvscaval.i	|- ( ph -> I e. W )
5		frlmvscaval.a	|- ( ph -> A e. K )
6		frlmvscaval.x	|- ( ph -> X e. B )
7		frlmvscaval.j	|- ( ph -> J e. I )
8		frlmvscaval.v	|- .xb = ( .s ` Y )
9		frlmvscaval.t	|- .x. = ( .r ` R )
10	1 2 3 4 5 6 8 9	frlmvscafval	|- ( ph -> ( A .xb X ) = ( ( I X. { A } ) oF .x. X ) )
11	10	fveq1d	|- ( ph -> ( ( A .xb X ) ` J ) = ( ( ( I X. { A } ) oF .x. X ) ` J ) )
12		fnconstg	|- ( A e. K -> ( I X. { A } ) Fn I )
13	5 12	syl	|- ( ph -> ( I X. { A } ) Fn I )
14	1 3 2	frlmbasf	|- ( ( I e. W /\ X e. B ) -> X : I --> K )
15	4 6 14	syl2anc	|- ( ph -> X : I --> K )
16	15	ffnd	|- ( ph -> X Fn I )
17		fnfvof	|- ( ( ( ( I X. { A } ) Fn I /\ X Fn I ) /\ ( I e. W /\ J e. I ) ) -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) )
18	13 16 4 7 17	syl22anc	|- ( ph -> ( ( ( I X. { A } ) oF .x. X ) ` J ) = ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) )
19		fvconst2g	|- ( ( A e. K /\ J e. I ) -> ( ( I X. { A } ) ` J ) = A )
20	5 7 19	syl2anc	|- ( ph -> ( ( I X. { A } ) ` J ) = A )
21	20	oveq1d	|- ( ph -> ( ( ( I X. { A } ) ` J ) .x. ( X ` J ) ) = ( A .x. ( X ` J ) ) )
22	11 18 21	3eqtrd	|- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )