This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )