Metamath Proof Explorer


Theorem isabli

Description: Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011)

Ref Expression
Hypotheses isabli.g GGrp
isabli.b B=BaseG
isabli.p +˙=+G
isabli.c xByBx+˙y=y+˙x
Assertion isabli GAbel

Proof

Step Hyp Ref Expression
1 isabli.g GGrp
2 isabli.b B=BaseG
3 isabli.p +˙=+G
4 isabli.c xByBx+˙y=y+˙x
5 4 rgen2 xByBx+˙y=y+˙x
6 2 3 isabl2 GAbelGGrpxByBx+˙y=y+˙x
7 1 5 6 mpbir2an GAbel