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 Xs_ R )
	prdscmnd.i	|- ( ph -> I e. W )
	prdscmnd.s	|- ( ph -> S e. V )
	prdsgabld.r	|- ( ph -> R : I --> Abel )
Assertion	prdsabld	|- ( ph -> Y e. Abel )

Proof

Step	Hyp	Ref	Expression
1		prdscmnd.y	|- Y = ( S Xs_ R )
2		prdscmnd.i	|- ( ph -> I e. W )
3		prdscmnd.s	|- ( ph -> S e. V )
4		prdsgabld.r	|- ( ph -> R : I --> Abel )
5		ablgrp	|- ( a e. Abel -> a e. Grp )
6	5	ssriv	|- Abel C_ Grp
7		fss	|- ( ( R : I --> Abel /\ Abel C_ Grp ) -> R : I --> Grp )
8	4 6 7	sylancl	|- ( ph -> R : I --> Grp )
9	1 2 3 8	prdsgrpd	|- ( ph -> Y e. Grp )
10		ablcmn	|- ( a e. Abel -> a e. CMnd )
11	10	ssriv	|- Abel C_ CMnd
12		fss	|- ( ( R : I --> Abel /\ Abel C_ CMnd ) -> R : I --> CMnd )
13	4 11 12	sylancl	|- ( ph -> R : I --> CMnd )
14	1 2 3 13	prdscmnd	|- ( ph -> Y e. CMnd )
15		isabl	|- ( Y e. Abel <-> ( Y e. Grp /\ Y e. CMnd ) )
16	9 14 15	sylanbrc	|- ( ph -> Y e. Abel )