Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablogrpo Structured version   Visualization version   GIF version

Theorem ablogrpo 28334
 Description: An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
ablogrpo (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Proof of Theorem ablogrpo
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2801 . . 3 ran 𝐺 = ran 𝐺
21isablo 28333 . 2 (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺(𝑥𝐺𝑦) = (𝑦𝐺𝑥)))
32simplbi 501 1 (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ran crn 5524  (class class class)co 7139  GrpOpcgr 28276  AbelOpcablo 28331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-cnv 5531  df-dm 5533  df-rn 5534  df-iota 6287  df-fv 6336  df-ov 7142  df-ablo 28332 This theorem is referenced by:  ablo32  28336  ablo4  28337  ablomuldiv  28339  ablodivdiv  28340  ablodivdiv4  28341  ablonncan  28343  ablonnncan1  28344  vcgrp  28357  isvcOLD  28366  isvciOLD  28367  cnidOLD  28369  nvgrp  28404  cnnv  28464  cnnvba  28466  cncph  28606  hilid  28948  hhnv  28952  hhba  28954  hhph  28965  hhssabloilem  29048  hhssnv  29051  ablo4pnp  35317  rngogrpo  35347  iscringd  35435
 Copyright terms: Public domain W3C validator