Metamath Proof Explorer

Theorem prdsplusgval

Description: Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015) (Revised by Mario Carneiro, 15-Aug-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$
		prdsplusgval.p	$⊢ \underset{˙}{+} = +_{Y}$
	Assertion	prdsplusgval	$⊢ φ \to F \underset{˙}{+} G = (x \in I ⟼ F (x) +_{R (x)} G (x))$

Proof

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		prdsplusgval.p	$⊢ \underset{˙}{+} = +_{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	prdsplusg	$⊢ φ \to \underset{˙}{+} = (y \in B, z \in B ⟼ (x \in I ⟼ y (x) +_{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) +_{R (x)} z (x) = F (x) +_{R (x)} G (x)$
16	15	adantl	$⊢ (φ \land (y = F \land z = G)) \to y (x) +_{R (x)} z (x) = F (x) +_{R (x)} G (x)$
17	16	mpteq2dv	$⊢ (φ \land (y = F \land z = G)) \to (x \in I ⟼ y (x) +_{R (x)} z (x)) = (x \in I ⟼ F (x) +_{R (x)} G (x))$
18	4	mptexd	$⊢ φ \to (x \in I ⟼ F (x) +_{R (x)} G (x)) \in V$
19	12 17 6 7 18	ovmpod	$⊢ φ \to F \underset{˙}{+} G = (x \in I ⟼ F (x) +_{R (x)} G (x))$