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 = {Base}_{Y}$
	prdsvscaval.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	prdsvscaval.k	$⊢ K = {Base}_{S}$
	prdsvscaval.s	$⊢ φ \to S \in V$
	prdsvscaval.i	$⊢ φ \to I \in W$
	prdsvscaval.r	$⊢ φ \to R Fn I$
	prdsvscaval.f	$⊢ φ \to F \in K$
	prdsvscaval.g	$⊢ φ \to G \in B$
	prdsvscafval.j	$⊢ φ \to J \in I$
Assertion	prdsvscafval	$⊢ φ \to (F \underset{˙}{\cdot} G) (J) = F \cdot_{R (J)} G (J)$

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

Metamath Proof Explorer