Theorem prdsgrpd

Description: The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsgrpd.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsgrpd.i	$$⊢\phi \to I\in W$$
	prdsgrpd.s	$$⊢\phi \to S\in V$$
	prdsgrpd.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
Assertion	prdsgrpd	$$⊢\phi \to Y\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		prdsgrpd.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsgrpd.i	$$⊢\phi \to I\in W$$
3		prdsgrpd.s	$$⊢\phi \to S\in V$$
4		prdsgrpd.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
5		eqidd	$$⊢\phi \to {\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
6		eqidd	$$⊢\phi \to {+}_Y={+}_Y$$
7		grpmnd	$$⊢a\in \mathrm{Grp}\to a\in \mathrm{Mnd}$$
8	7	ssriv	$$⊢\mathrm{Grp}\subseteq \mathrm{Mnd}$$
9		fss	$$⊢\left(R:I⟶\mathrm{Grp}\wedge \mathrm{Grp}\subseteq \mathrm{Mnd}\right)\to R:I⟶\mathrm{Mnd}$$
10	4 8 9	sylancl	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
11	1 2 3 10	prds0g	$$⊢\phi \to 0_{𝑔}\circ R=0_Y$$
12	1 2 3 10	prdsmndd	$$⊢\phi \to Y\in \mathrm{Mnd}$$
13		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
14		eqid	$$⊢{+}_Y={+}_Y$$
15	3	elexd	$$⊢\phi \to S\in \mathrm{V}$$
16	15	adantr	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to S\in \mathrm{V}$$
17	2	elexd	$$⊢\phi \to I\in \mathrm{V}$$
18	17	adantr	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to I\in \mathrm{V}$$
19	4	adantr	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to R:I⟶\mathrm{Grp}$$
20		simpr	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to a\in {\mathrm{Base}}_Y$$
21		eqid	$$⊢0_{𝑔}\circ R=0_{𝑔}\circ R$$
22		eqid	$$⊢\left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right)=\left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right)$$
23	1 13 14 16 18 19 20 21 22	prdsinvlem	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to \left(\left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right)\in {\mathrm{Base}}_Y\wedge \left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right){+}_{Y}a=0_{𝑔}\circ R\right)$$
24	23	simpld	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to \left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right)\in {\mathrm{Base}}_Y$$
25	23	simprd	$$⊢\left(\phi \wedge a\in {\mathrm{Base}}_Y\right)\to \left(b\in I⟼{inv}_g\left(R\left(b\right)\right)\left(a\left(b\right)\right)\right){+}_{Y}a=0_{𝑔}\circ R$$
26	5 6 11 12 24 25	isgrpd2	$$⊢\phi \to Y\in \mathrm{Grp}$$