prdsmulrval

Description: Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsbasmpt.b	$⊢ B = {Base}_{Y}$
	prdsbasmpt.s	$⊢ φ \to S \in V$
	prdsbasmpt.i	$⊢ φ \to I \in W$
	prdsbasmpt.r	$⊢ φ \to R Fn I$
	prdsplusgval.f	$⊢ φ \to F \in B$
	prdsplusgval.g	$⊢ φ \to G \in B$
	prdsmulrval.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
Assertion	prdsmulrval	$⊢ φ \to F \underset{˙}{\cdot} G = (x \in I ⟼ F (x) \cdot_{R (x)} G (x))$

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsbasmpt.b	$⊢ B = {Base}_{Y}$
3		prdsbasmpt.s	$⊢ φ \to S \in V$
4		prdsbasmpt.i	$⊢ φ \to I \in W$
5		prdsbasmpt.r	$⊢ φ \to R Fn I$
6		prdsplusgval.f	$⊢ φ \to F \in B$
7		prdsplusgval.g	$⊢ φ \to G \in B$
8		prdsmulrval.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		fnex	$⊢ (R Fn I \land I \in W) \to R \in V$
10	5 4 9	syl2anc	$⊢ φ \to R \in V$
11	5	fndmd	$⊢ φ \to dom R = I$
12	1 3 10 2 11 8	prdsmulr	$⊢ φ \to \underset{˙}{\cdot} = (y \in B, z \in B ⟼ (x \in I ⟼ y (x) \cdot_{R (x)} z (x)))$
13		fveq1	$⊢ y = F \to y (x) = F (x)$
14		fveq1	$⊢ z = G \to z (x) = G (x)$
15	13 14	oveqan12d	$⊢ (y = F \land z = G) \to y (x) \cdot_{R (x)} z (x) = F (x) \cdot_{R (x)} G (x)$
16	15	adantl	$⊢ (φ \land (y = F \land z = G)) \to y (x) \cdot_{R (x)} z (x) = F (x) \cdot_{R (x)} G (x)$
17	16	mpteq2dv	$⊢ (φ \land (y = F \land z = G)) \to (x \in I ⟼ y (x) \cdot_{R (x)} z (x)) = (x \in I ⟼ F (x) \cdot_{R (x)} G (x))$
18	4	mptexd	$⊢ φ \to (x \in I ⟼ F (x) \cdot_{R (x)} G (x)) \in V$
19	12 17 6 7 18	ovmpod	$⊢ φ \to F \underset{˙}{\cdot} G = (x \in I ⟼ F (x) \cdot_{R (x)} G (x))$

Metamath Proof Explorer