Metamath Proof Explorer

Theorem ablnsg

Description: Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Assertion ablnsg 
|- ( G e. Abel -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 1 2 ablcom 
 |-  ( ( G e. Abel /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) )
4 3 3expb 
 |-  ( ( G e. Abel /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) )
5 4 eleq1d 
 |-  ( ( G e. Abel /\ ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( y ( +g ` G ) z ) e. x <-> ( z ( +g ` G ) y ) e. x ) )
6 5 ralrimivva 
 |-  ( G e. Abel -> A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) e. x <-> ( z ( +g ` G ) y ) e. x ) )
7 1 2 isnsg 
 |-  ( x e. ( NrmSGrp ` G ) <-> ( x e. ( SubGrp ` G ) /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) e. x <-> ( z ( +g ` G ) y ) e. x ) ) )
8 7 rbaib 
 |-  ( A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) e. x <-> ( z ( +g ` G ) y ) e. x ) -> ( x e. ( NrmSGrp ` G ) <-> x e. ( SubGrp ` G ) ) )
9 6 8 syl 
 |-  ( G e. Abel -> ( x e. ( NrmSGrp ` G ) <-> x e. ( SubGrp ` G ) ) )
10 9 eqrdv 
 |-  ( G e. Abel -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )