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 )