Metamath Proof Explorer


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 )