prdsvscaval

Description: Scalar multiplication in a structure product is pointwise. (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$
Assertion	prdsvscaval	$⊢ φ \to F \underset{˙}{\cdot} G = (x \in I ⟼ F \cdot_{R (x)} G (x))$

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		fnex	$⊢ (R Fn I \land I \in W) \to R \in V$
11	7 6 10	syl2anc	$⊢ φ \to R \in V$
12	7	fndmd	$⊢ φ \to dom R = I$
13	1 5 11 2 12 4 3	prdsvsca	$⊢ φ \to \underset{˙}{\cdot} = (y \in K, z \in B ⟼ (x \in I ⟼ y \cdot_{R (x)} z (x)))$
14		id	$⊢ y = F \to y = F$
15		fveq1	$⊢ z = G \to z (x) = G (x)$
16	14 15	oveqan12d	$⊢ (y = F \land z = G) \to y \cdot_{R (x)} z (x) = F \cdot_{R (x)} G (x)$
17	16	adantl	$⊢ (φ \land (y = F \land z = G)) \to y \cdot_{R (x)} z (x) = F \cdot_{R (x)} G (x)$
18	17	mpteq2dv	$⊢ (φ \land (y = F \land z = G)) \to (x \in I ⟼ y \cdot_{R (x)} z (x)) = (x \in I ⟼ F \cdot_{R (x)} G (x))$
19	6	mptexd	$⊢ φ \to (x \in I ⟼ F \cdot_{R (x)} G (x)) \in V$
20	13 18 8 9 19	ovmpod	$⊢ φ \to F \underset{˙}{\cdot} G = (x \in I ⟼ F \cdot_{R (x)} G (x))$

Metamath Proof Explorer