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 ⊢ 𝑌 = ( 𝑆 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 )