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 ⨉ 𝑠 R
prdscmnd.i ⊢ φ → I ∈ W
prdscmnd.s ⊢ φ → S ∈ V
prdsgabld.r ⊢ φ → R : I ⟶ Abel
Assertion prdsabld ⊢ φ → Y ∈ Abel

Proof

Step Hyp Ref Expression
1 prdscmnd.y ⊢ Y = S ⨉ 𝑠 R
2 prdscmnd.i ⊢ φ → I ∈ W
3 prdscmnd.s ⊢ φ → S ∈ V
4 prdsgabld.r ⊢ φ → R : I ⟶ Abel
5 ablgrp ⊢ a ∈ Abel → a ∈ Grp
6 5 ssriv ⊢ Abel ⊆ Grp
7 fss ⊢ R : I ⟶ Abel ∧ Abel ⊆ Grp → R : I ⟶ Grp
8 4 6 7 sylancl ⊢ φ → R : I ⟶ Grp
9 1 2 3 8 prdsgrpd ⊢ φ → Y ∈ Grp
10 ablcmn ⊢ a ∈ Abel → a ∈ CMnd
11 10 ssriv ⊢ Abel ⊆ CMnd
12 fss ⊢ R : I ⟶ Abel ∧ Abel ⊆ CMnd → R : I ⟶ CMnd
13 4 11 12 sylancl ⊢ φ → R : I ⟶ CMnd
14 1 2 3 13 prdscmnd ⊢ φ → Y ∈ CMnd
15 isabl ⊢ Y ∈ Abel ↔ Y ∈ Grp ∧ Y ∈ CMnd
16 9 14 15 sylanbrc ⊢ φ → Y ∈ Abel