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{\uparrow }_{𝑠}I$$
	pwsvscaval.b	$$⊢B={\mathrm{Base}}_Y$$
	pwsvscaval.s	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	pwsvscaval.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
	pwsvscaval.f	$$⊢F=\mathrm{Scalar}\left(R\right)$$
	pwsvscaval.k	$$⊢K={\mathrm{Base}}_F$$
	pwsvscaval.r	$$⊢\phi \to R\in V$$
	pwsvscaval.i	$$⊢\phi \to I\in W$$
	pwsvscaval.a	$$⊢\phi \to A\in K$$
	pwsvscaval.x	$$⊢\phi \to X\in B$$
	pwsvscaval.j	$$⊢\phi \to J\in I$$
Assertion	pwsvscaval	$$⊢\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		pwsvscaval.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsvscaval.b	$$⊢B={\mathrm{Base}}_Y$$
3		pwsvscaval.s	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		pwsvscaval.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
5		pwsvscaval.f	$$⊢F=\mathrm{Scalar}\left(R\right)$$
6		pwsvscaval.k	$$⊢K={\mathrm{Base}}_F$$
7		pwsvscaval.r	$$⊢\phi \to R\in V$$
8		pwsvscaval.i	$$⊢\phi \to I\in W$$
9		pwsvscaval.a	$$⊢\phi \to A\in K$$
10		pwsvscaval.x	$$⊢\phi \to X\in B$$
11		pwsvscaval.j	$$⊢\phi \to J\in I$$
12	1 2 3 4 5 6 7 8 9 10	pwsvscafval	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X$$
13	12	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)$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	1 14 2 7 8 10	pwselbas	$$⊢\phi \to X:I⟶{\mathrm{Base}}_R$$
16	15	ffnd	$$⊢\phi \to XFnI$$
17		eqidd	$$⊢\left(\phi \wedge J\in I\right)\to X\left(J\right)=X\left(J\right)$$
18	8 9 16 17	ofc1	$$⊢\left(\phi \wedge J\in I\right)\to \left(\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X\right)\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$
19	11 18	mpdan	$$⊢\phi \to \left(\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X\right)\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$
20	13 19	eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=A\underset{\dot{}}{·}X\left(J\right)$$