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

Theorem ablogrpo 23922
Description: An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
ablogrpo  |-  ( G  e.  AbelOp  ->  G  e.  GrpOp )

Proof of Theorem ablogrpo
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2454 . . 3  |-  ran  G  =  ran  G
21isablo 23921 . 2  |-  ( G  e.  AbelOp 
<->  ( G  e.  GrpOp  /\ 
A. x  e.  ran  G A. y  e.  ran  G ( x G y )  =  ( y G x ) ) )
32simplbi 460 1  |-  ( G  e.  AbelOp  ->  G  e.  GrpOp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   A.wral 2798   ran crn 4948  (class class class)co 6199   GrpOpcgr 23824   AbelOpcablo 23919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-cnv 4955  df-dm 4957  df-rn 4958  df-iota 5488  df-fv 5533  df-ov 6202  df-ablo 23920
This theorem is referenced by:  ablo32  23924  ablo4  23925  ablomuldiv  23927  ablodivdiv  23928  ablodivdiv4  23929  ablonnncan  23931  ablonncan  23932  ablonnncan1  23933  gxdi  23934  cnid  23989  addinv  23990  readdsubgo  23991  zaddsubgo  23992  mulid  23994  ghablo  24007  efghgrp  24011  rngogrpo  24028  cnrngo  24041  rngosn  24042  vcgrp  24087  vcoprnelem  24107  isvc  24110  isvci  24111  nvgrp  24146  cnnv  24218  cnnvba  24220  cncph  24370  hilid  24714  hhnv  24718  hhba  24720  hhph  24731  hhssabloi  24814  hhssnv  24816  ablo4pnp  28892  iscringd  28946
  Copyright terms: Public domain W3C validator