Theorem prdsabld

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

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

Proof

Step	Hyp	Ref	Expression
1		prdscmnd.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdscmnd.i	$$⊢\phi \to I\in W$$
3		prdscmnd.s	$$⊢\phi \to S\in V$$
4		prdsgabld.r	$$⊢\phi \to R:I⟶\mathrm{Abel}$$
5		ablgrp	$$⊢a\in \mathrm{Abel}\to a\in \mathrm{Grp}$$
6	5	ssriv	$$⊢\mathrm{Abel}\subseteq \mathrm{Grp}$$
7		fss	$$⊢\left(R:I⟶\mathrm{Abel}\wedge \mathrm{Abel}\subseteq \mathrm{Grp}\right)\to R:I⟶\mathrm{Grp}$$
8	4 6 7	sylancl	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
9	1 2 3 8	prdsgrpd	$$⊢\phi \to Y\in \mathrm{Grp}$$
10		ablcmn	$$⊢a\in \mathrm{Abel}\to a\in \mathrm{CMnd}$$
11	10	ssriv	$$⊢\mathrm{Abel}\subseteq \mathrm{CMnd}$$
12		fss	$$⊢\left(R:I⟶\mathrm{Abel}\wedge \mathrm{Abel}\subseteq \mathrm{CMnd}\right)\to R:I⟶\mathrm{CMnd}$$
13	4 11 12	sylancl	$$⊢\phi \to R:I⟶\mathrm{CMnd}$$
14	1 2 3 13	prdscmnd	$$⊢\phi \to Y\in \mathrm{CMnd}$$
15		isabl	$$⊢Y\in \mathrm{Abel}\leftrightarrow \left(Y\in \mathrm{Grp}\wedge Y\in \mathrm{CMnd}\right)$$
16	9 14 15	sylanbrc	$$⊢\phi \to Y\in \mathrm{Abel}$$