prdsgrpd

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

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

Metamath Proof Explorer