Metamath Proof Explorer


Theorem isabloi

Description: Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isabli.1 GGrpOp
isabli.2 domG=X×X
isabli.3 xXyXxGy=yGx
Assertion isabloi GAbelOp

Proof

Step Hyp Ref Expression
1 isabli.1 GGrpOp
2 isabli.2 domG=X×X
3 isabli.3 xXyXxGy=yGx
4 3 rgen2 xXyXxGy=yGx
5 1 2 grporn X=ranG
6 5 isablo GAbelOpGGrpOpxXyXxGy=yGx
7 1 4 6 mpbir2an GAbelOp