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\mathrm{freeLMod}I$$
	frlmvscaval.b	$$⊢B={\mathrm{Base}}_Y$$
	frlmvscaval.k	$$⊢K={\mathrm{Base}}_R$$
	frlmvscaval.i	$$⊢\phi \to I\in W$$
	frlmvscaval.a	$$⊢\phi \to A\in K$$
	frlmvscaval.x	$$⊢\phi \to X\in B$$
	frlmvscaval.j	$$⊢\phi \to J\in I$$
	frlmvscaval.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
	frlmvscaval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	frlmvscaval	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmvscaval.y	$$⊢Y=R\mathrm{freeLMod}I$$
2		frlmvscaval.b	$$⊢B={\mathrm{Base}}_Y$$
3		frlmvscaval.k	$$⊢K={\mathrm{Base}}_R$$
4		frlmvscaval.i	$$⊢\phi \to I\in W$$
5		frlmvscaval.a	$$⊢\phi \to A\in K$$
6		frlmvscaval.x	$$⊢\phi \to X\in B$$
7		frlmvscaval.j	$$⊢\phi \to J\in I$$
8		frlmvscaval.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
9		frlmvscaval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
10	1 2 3 4 5 6 8 9	frlmvscafval	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X$$
11	10	fveq1d	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=\left(\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X\right)\left(J\right)$$
12		fnconstg	$$⊢A\in K\to \left(I\times \left\{A\right\}\right)FnI$$
13	5 12	syl	$$⊢\phi \to \left(I\times \left\{A\right\}\right)FnI$$
14	1 3 2	frlmbasf	$$⊢\left(I\in W\wedge X\in B\right)\to X:I⟶K$$
15	4 6 14	syl2anc	$$⊢\phi \to X:I⟶K$$
16	15	ffnd	$$⊢\phi \to XFnI$$
17		fnfvof	$$⊢\left(\left(\left(I\times \left\{A\right\}\right)FnI\wedge XFnI\right)\wedge \left(I\in W\wedge J\in I\right)\right)\to \left(\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X\right)\left(J\right)=\left(I\times \left\{A\right\}\right)\left(J\right)\underset{\dot{}}{·}X\left(J\right)$$
18	13 16 4 7 17	syl22anc	$$⊢\phi \to \left(\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X\right)\left(J\right)=\left(I\times \left\{A\right\}\right)\left(J\right)\underset{\dot{}}{·}X\left(J\right)$$
19		fvconst2g	$$⊢\left(A\in K\wedge J\in I\right)\to \left(I\times \left\{A\right\}\right)\left(J\right)=A$$
20	5 7 19	syl2anc	$$⊢\phi \to \left(I\times \left\{A\right\}\right)\left(J\right)=A$$
21	20	oveq1d	$$⊢\phi \to \left(I\times \left\{A\right\}\right)\left(J\right)\underset{\dot{}}{·}X\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$
22	11 18 21	3eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$