# 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}=\mathrm{ran}{G}$
Assertion ablocom ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}={B}{G}{A}$

### Proof

Step Hyp Ref Expression
1 ablcom.1 ${⊢}{X}=\mathrm{ran}{G}$
2 1 isablo ${⊢}{G}\in \mathrm{AbelOp}↔\left({G}\in \mathrm{GrpOp}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{G}{y}={y}{G}{x}\right)$
3 2 simprbi ${⊢}{G}\in \mathrm{AbelOp}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{G}{y}={y}{G}{x}$
4 oveq1 ${⊢}{x}={A}\to {x}{G}{y}={A}{G}{y}$
5 oveq2 ${⊢}{x}={A}\to {y}{G}{x}={y}{G}{A}$
6 4 5 eqeq12d ${⊢}{x}={A}\to \left({x}{G}{y}={y}{G}{x}↔{A}{G}{y}={y}{G}{A}\right)$
7 oveq2 ${⊢}{y}={B}\to {A}{G}{y}={A}{G}{B}$
8 oveq1 ${⊢}{y}={B}\to {y}{G}{A}={B}{G}{A}$
9 7 8 eqeq12d ${⊢}{y}={B}\to \left({A}{G}{y}={y}{G}{A}↔{A}{G}{B}={B}{G}{A}\right)$
10 6 9 rspc2v ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{G}{y}={y}{G}{x}\to {A}{G}{B}={B}{G}{A}\right)$
11 3 10 syl5com ${⊢}{G}\in \mathrm{AbelOp}\to \left(\left({A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}={B}{G}{A}\right)$
12 11 3impib ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}={B}{G}{A}$