# Metamath Proof Explorer

## Theorem isablo

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

Ref Expression
Hypothesis isabl.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 isabl.1 ${⊢}{X}=\mathrm{ran}{G}$
2 rneq ${⊢}{g}={G}\to \mathrm{ran}{g}=\mathrm{ran}{G}$
3 2 1 syl6eqr ${⊢}{g}={G}\to \mathrm{ran}{g}={X}$
4 raleq ${⊢}\mathrm{ran}{g}={X}\to \left(\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}\right)$
5 4 raleqbi1dv ${⊢}\mathrm{ran}{g}={X}\to \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}\right)$
6 3 5 syl ${⊢}{g}={G}\to \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}\right)$
7 oveq ${⊢}{g}={G}\to {x}{g}{y}={x}{G}{y}$
8 oveq ${⊢}{g}={G}\to {y}{g}{x}={y}{G}{x}$
9 7 8 eqeq12d ${⊢}{g}={G}\to \left({x}{g}{y}={y}{g}{x}↔{x}{G}{y}={y}{G}{x}\right)$
10 9 2ralbidv ${⊢}{g}={G}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{G}{y}={y}{G}{x}\right)$
11 6 10 bitrd ${⊢}{g}={G}\to \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{G}{y}={y}{G}{x}\right)$
12 df-ablo ${⊢}\mathrm{AbelOp}=\left\{{g}\in \mathrm{GrpOp}|\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}\right\}$
13 11 12 elrab2 ${⊢}{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)$