Metamath Proof Explorer

Theorem subgabl

Description: A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypothesis subgabl.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion subgabl ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )

Proof

Step Hyp Ref Expression
1 subgabl.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 1 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
3 2 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 1 4 ressplusg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
6 5 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
7 1 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
8 7 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Grp )
9 simp1l ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝐺 ∈ Abel )
10 simp1r ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 11 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 10 12 syl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
14 simp2 ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
15 13 14 sseldd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
16 simp3 ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
17 13 16 sseldd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
18 11 4 ablcom ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
19 9 15 17 18 syl3anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
20 3 6 8 19 isabld ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )