Metamath Proof Explorer

Definition df-ablo

Description: Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion 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\}$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cablo ${class}\mathrm{AbelOp}$
1 vg ${setvar}{g}$
2 cgr ${class}\mathrm{GrpOp}$
3 vx ${setvar}{x}$
4 1 cv ${setvar}{g}$
5 4 crn ${class}\mathrm{ran}{g}$
6 vy ${setvar}{y}$
7 3 cv ${setvar}{x}$
8 6 cv ${setvar}{y}$
9 7 8 4 co ${class}\left({x}{g}{y}\right)$
10 8 7 4 co ${class}\left({y}{g}{x}\right)$
11 9 10 wceq ${wff}{x}{g}{y}={y}{g}{x}$
12 11 6 5 wral ${wff}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={y}{g}{x}$
13 12 3 5 wral ${wff}\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}$
14 13 1 2 crab ${class}\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\}$
15 0 14 wceq ${wff}\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\}$