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 GAbelNrmSGrpG=SubGrpG

Proof

Step Hyp Ref Expression
1 eqid BaseG=BaseG
2 eqid +G=+G
3 1 2 ablcom GAbelyBaseGzBaseGy+Gz=z+Gy
4 3 3expb GAbelyBaseGzBaseGy+Gz=z+Gy
5 4 eleq1d GAbelyBaseGzBaseGy+Gzxz+Gyx
6 5 ralrimivva GAbelyBaseGzBaseGy+Gzxz+Gyx
7 1 2 isnsg xNrmSGrpGxSubGrpGyBaseGzBaseGy+Gzxz+Gyx
8 7 rbaib yBaseGzBaseGy+Gzxz+GyxxNrmSGrpGxSubGrpG
9 6 8 syl GAbelxNrmSGrpGxSubGrpG
10 9 eqrdv GAbelNrmSGrpG=SubGrpG