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 
|- H = ( G |`s S )
Assertion subgabl 
|- ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Abel )

Proof

Step Hyp Ref Expression
1 subgabl.h 
 |-  H = ( G |`s S )
2 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
3 2 adantl 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> S = ( Base ` H ) )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 1 4 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
6 5 adantl 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( +g ` G ) = ( +g ` H ) )
7 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
8 7 adantl 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Grp )
9 simp1l 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> G e. Abel )
10 simp1r 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> S e. ( SubGrp ` G ) )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 11 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
13 10 12 syl 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> S C_ ( Base ` G ) )
14 simp2 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> x e. S )
15 13 14 sseldd 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> x e. ( Base ` G ) )
16 simp3 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> y e. S )
17 13 16 sseldd 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> y e. ( Base ` G ) )
18 11 4 ablcom 
 |-  ( ( G e. Abel /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
19 9 15 17 18 syl3anc 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ x e. S /\ y e. S ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
20 3 6 8 19 isabld 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> H e. Abel )