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 ) )