Theorem prdsplusgcl

Description: Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsplusgcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsplusgcl.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsplusgcl.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	prdsplusgcl.s	$$⊢\phi \to S\in V$$
	prdsplusgcl.i	$$⊢\phi \to I\in W$$
	prdsplusgcl.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
	prdsplusgcl.f	$$⊢\phi \to F\in B$$
	prdsplusgcl.g	$$⊢\phi \to G\in B$$
Assertion	prdsplusgcl	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$

Proof

Step	Hyp	Ref	Expression
1		prdsplusgcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsplusgcl.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsplusgcl.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
4		prdsplusgcl.s	$$⊢\phi \to S\in V$$
5		prdsplusgcl.i	$$⊢\phi \to I\in W$$
6		prdsplusgcl.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
7		prdsplusgcl.f	$$⊢\phi \to F\in B$$
8		prdsplusgcl.g	$$⊢\phi \to G\in B$$
9	6	ffnd	$$⊢\phi \to RFnI$$
10	1 2 4 5 9 7 8 3	prdsplusgval	$$⊢\phi \to F\underset{\dot{}}{+}G=\left(x\in I⟼F\left(x\right){+}_{R\left(x\right)}G\left(x\right)\right)$$
11	6	ffvelrnda	$$⊢\left(\phi \wedge x\in I\right)\to R\left(x\right)\in \mathrm{Mnd}$$
12	4	adantr	$$⊢\left(\phi \wedge x\in I\right)\to S\in V$$
13	5	adantr	$$⊢\left(\phi \wedge x\in I\right)\to I\in W$$
14	9	adantr	$$⊢\left(\phi \wedge x\in I\right)\to RFnI$$
15	7	adantr	$$⊢\left(\phi \wedge x\in I\right)\to F\in B$$
16		simpr	$$⊢\left(\phi \wedge x\in I\right)\to x\in I$$
17	1 2 12 13 14 15 16	prdsbasprj	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
18	8	adantr	$$⊢\left(\phi \wedge x\in I\right)\to G\in B$$
19	1 2 12 13 14 18 16	prdsbasprj	$$⊢\left(\phi \wedge x\in I\right)\to G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
20		eqid	$$⊢{\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{R\left(x\right)}$$
21		eqid	$$⊢{+}_{R\left(x\right)}={+}_{R\left(x\right)}$$
22	20 21	mndcl	$$⊢\left(R\left(x\right)\in \mathrm{Mnd}\wedge F\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\wedge G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)\to F\left(x\right){+}_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
23	11 17 19 22	syl3anc	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right){+}_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
24	23	ralrimiva	$$⊢\phi \to \forall x\in IF\left(x\right){+}_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
25	1 2 4 5 9	prdsbasmpt	$$⊢\phi \to \left(\left(x\in I⟼F\left(x\right){+}_{R\left(x\right)}G\left(x\right)\right)\in B\leftrightarrow \forall x\in IF\left(x\right){+}_{R\left(x\right)}G\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)$$
26	24 25	mpbird	$$⊢\phi \to \left(x\in I⟼F\left(x\right){+}_{R\left(x\right)}G\left(x\right)\right)\in B$$
27	10 26	eqeltrd	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$