This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ G ∈ GrpOp
isabli.2 ⊢ dom ⁡ G = X × X
isabli.3 ⊢ x ∈ X ∧ y ∈ X → x G y = y G x
Assertion isabloi ⊢ G ∈ AbelOp

Proof

Step Hyp Ref Expression
1 isabli.1 ⊢ G ∈ GrpOp
2 isabli.2 ⊢ dom ⁡ G = X × X
3 isabli.3 ⊢ x ∈ X ∧ y ∈ X → x G y = y G x
4 3 rgen2 ⊢ ∀ x ∈ X ∀ y ∈ X x G y = y G x
5 1 2 grporn ⊢ X = ran ⁡ G
6 5 isablo ⊢ G ∈ AbelOp ↔ G ∈ GrpOp ∧ ∀ x ∈ X ∀ y ∈ X x G y = y G x
7 1 4 6 mpbir2an ⊢ G ∈ AbelOp