Metamath Proof Explorer

Theorem ablocom

Description: An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 ⊢ X = ran ⁡ G
Assertion ablocom ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A G B = B G A

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢ X = ran ⁡ G
2 1 isablo ⊢ G ∈ AbelOp ↔ G ∈ GrpOp ∧ ∀ x ∈ X ∀ y ∈ X x G y = y G x
3 2 simprbi ⊢ G ∈ AbelOp → ∀ x ∈ X ∀ y ∈ X x G y = y G x
4 oveq1 ⊢ x = A → x G y = A G y
5 oveq2 ⊢ x = A → y G x = y G A
6 4 5 eqeq12d ⊢ x = A → x G y = y G x ↔ A G y = y G A
7 oveq2 ⊢ y = B → A G y = A G B
8 oveq1 ⊢ y = B → y G A = B G A
9 7 8 eqeq12d ⊢ y = B → A G y = y G A ↔ A G B = B G A
10 6 9 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X x G y = y G x → A G B = B G A
11 3 10 syl5com ⊢ G ∈ AbelOp → A ∈ X ∧ B ∈ X → A G B = B G A
12 11 3impib ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A G B = B G A