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	$$⊢G\in \mathrm{GrpOp}$$
	isabli.2	$$⊢\mathrm{dom}G=X\times X$$
	isabli.3	$$⊢\left(x\in X\wedge y\in X\right)\to xGy=yGx$$
Assertion	isabloi	$$⊢G\in \mathrm{AbelOp}$$

Proof

Step	Hyp	Ref	Expression
1		isabli.1	$$⊢G\in \mathrm{GrpOp}$$
2		isabli.2	$$⊢\mathrm{dom}G=X\times X$$
3		isabli.3	$$⊢\left(x\in X\wedge y\in X\right)\to xGy=yGx$$
4	3	rgen2	$$⊢\forall x\in X\forall y\in XxGy=yGx$$
5	1 2	grporn	$$⊢X=\mathrm{ran}G$$
6	5	isablo	$$⊢G\in \mathrm{AbelOp}\leftrightarrow \left(G\in \mathrm{GrpOp}\wedge \forall x\in X\forall y\in XxGy=yGx\right)$$
7	1 4 6	mpbir2an	$$⊢G\in \mathrm{AbelOp}$$