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{⨉}_{𝑠}R$$
	prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsvscaval.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	prdsvscaval.k	$$⊢K={\mathrm{Base}}_S$$
	prdsvscaval.s	$$⊢\phi \to S\in V$$
	prdsvscaval.i	$$⊢\phi \to I\in W$$
	prdsvscaval.r	$$⊢\phi \to RFnI$$
	prdsvscaval.f	$$⊢\phi \to F\in K$$
	prdsvscaval.g	$$⊢\phi \to G\in B$$
	prdsvscafval.j	$$⊢\phi \to J\in I$$
Assertion	prdsvscafval	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\left(J\right)=F{\cdot }_{R\left(J\right)}G\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsvscaval.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4		prdsvscaval.k	$$⊢K={\mathrm{Base}}_S$$
5		prdsvscaval.s	$$⊢\phi \to S\in V$$
6		prdsvscaval.i	$$⊢\phi \to I\in W$$
7		prdsvscaval.r	$$⊢\phi \to RFnI$$
8		prdsvscaval.f	$$⊢\phi \to F\in K$$
9		prdsvscaval.g	$$⊢\phi \to G\in B$$
10		prdsvscafval.j	$$⊢\phi \to J\in I$$
11	1 2 3 4 5 6 7 8 9	prdsvscaval	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(x\in I⟼F{\cdot }_{R\left(x\right)}G\left(x\right)\right)$$
12		2fveq3	$$⊢x=J\to {\cdot }_{R\left(x\right)}={\cdot }_{R\left(J\right)}$$
13		eqidd	$$⊢x=J\to F=F$$
14		fveq2	$$⊢x=J\to G\left(x\right)=G\left(J\right)$$
15	12 13 14	oveq123d	$$⊢x=J\to F{\cdot }_{R\left(x\right)}G\left(x\right)=F{\cdot }_{R\left(J\right)}G\left(J\right)$$
16	15	adantl	$$⊢\left(\phi \wedge x=J\right)\to F{\cdot }_{R\left(x\right)}G\left(x\right)=F{\cdot }_{R\left(J\right)}G\left(J\right)$$
17		ovexd	$$⊢\phi \to F{\cdot }_{R\left(J\right)}G\left(J\right)\in \mathrm{V}$$
18	11 16 10 17	fvmptd	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\left(J\right)=F{\cdot }_{R\left(J\right)}G\left(J\right)$$