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 𝑌 = ( 𝑆 Xs 𝑅 )
prdscmnd.i ( 𝜑𝐼𝑊 )
prdscmnd.s ( 𝜑𝑆𝑉 )
prdsgabld.r ( 𝜑𝑅 : 𝐼 ⟶ Abel )
Assertion prdsabld ( 𝜑𝑌 ∈ Abel )

Proof

Step Hyp Ref Expression
1 prdscmnd.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdscmnd.i ( 𝜑𝐼𝑊 )
3 prdscmnd.s ( 𝜑𝑆𝑉 )
4 prdsgabld.r ( 𝜑𝑅 : 𝐼 ⟶ Abel )
5 ablgrp ( 𝑎 ∈ Abel → 𝑎 ∈ Grp )
6 5 ssriv Abel ⊆ Grp
7 fss ( ( 𝑅 : 𝐼 ⟶ Abel ∧ Abel ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
8 4 6 7 sylancl ( 𝜑𝑅 : 𝐼 ⟶ Grp )
9 1 2 3 8 prdsgrpd ( 𝜑𝑌 ∈ Grp )
10 ablcmn ( 𝑎 ∈ Abel → 𝑎 ∈ CMnd )
11 10 ssriv Abel ⊆ CMnd
12 fss ( ( 𝑅 : 𝐼 ⟶ Abel ∧ Abel ⊆ CMnd ) → 𝑅 : 𝐼 ⟶ CMnd )
13 4 11 12 sylancl ( 𝜑𝑅 : 𝐼 ⟶ CMnd )
14 1 2 3 13 prdscmnd ( 𝜑𝑌 ∈ CMnd )
15 isabl ( 𝑌 ∈ Abel ↔ ( 𝑌 ∈ Grp ∧ 𝑌 ∈ CMnd ) )
16 9 14 15 sylanbrc ( 𝜑𝑌 ∈ Abel )