Theorem prdsplusgsgrpcl

Description: Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025)

	Ref	Expression
Hypotheses	prdsplusgsgrpcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsplusgsgrpcl.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsplusgsgrpcl.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	prdsplusgsgrpcl.s	$$⊢\phi \to S\in V$$
	prdsplusgsgrpcl.i	$$⊢\phi \to I\in W$$
	prdsplusgsgrpcl.r	No typesetting found for |- ( ph -> R : I --> Smgrp ) with typecode |-
	prdsplusgsgrpcl.f	$$⊢\phi \to F\in B$$
	prdsplusgsgrpcl.g	$$⊢\phi \to G\in B$$
Assertion	prdsplusgsgrpcl	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$

Proof

Step	Hyp	Ref	Expression
1		prdsplusgsgrpcl.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsplusgsgrpcl.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsplusgsgrpcl.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
4		prdsplusgsgrpcl.s	$$⊢\phi \to S\in V$$
5		prdsplusgsgrpcl.i	$$⊢\phi \to I\in W$$
6		prdsplusgsgrpcl.r	Could not format ( ph -> R : I --> Smgrp ) : No typesetting found for |- ( ph -> R : I --> Smgrp ) with typecode |-
7		prdsplusgsgrpcl.f	$$⊢\phi \to F\in B$$
8		prdsplusgsgrpcl.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	ffvelcdmda	Could not format ( ( ph /\ x e. I ) -> ( R ` x ) e. Smgrp ) : No typesetting found for |- ( ( ph /\ x e. I ) -> ( R ` x ) e. Smgrp ) with typecode |-
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	sgrpcl	Could not format ( ( ( R ` x ) e. Smgrp /\ ( F ` x ) e. ( Base ` ( R ` x ) ) /\ ( G ` x ) e. ( Base ` ( R ` x ) ) ) -> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) ) : No typesetting found for |- ( ( ( R ` x ) e. Smgrp /\ ( F ` x ) e. ( Base ` ( R ` x ) ) /\ ( G ` x ) e. ( Base ` ( R ` x ) ) ) -> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) e. ( Base ` ( R ` x ) ) ) with typecode |-
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$$