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

Theorem ablogrpo 21874
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 2438 . . 3  |-  ran  G  =  ran  G
21isablo 21873 . 2  |-  ( G  e.  AbelOp 
<->  ( G  e.  GrpOp  /\ 
A. x  e.  ran  G A. y  e.  ran  G ( x G y )  =  ( y G x ) ) )
32simplbi 448 1  |-  ( G  e.  AbelOp  ->  G  e.  GrpOp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   A.wral 2707   ran crn 4881  (class class class)co 6083   GrpOpcgr 21776   AbelOpcablo 21871
This theorem is referenced by:  ablo32  21876  ablo4  21877  ablomuldiv  21879  ablodivdiv  21880  ablodivdiv4  21881  ablonnncan  21883  ablonncan  21884  ablonnncan1  21885  gxdi  21886  cnid  21941  addinv  21942  readdsubgo  21943  zaddsubgo  21944  mulid  21946  ghablo  21959  efghgrp  21963  rngogrpo  21980  cnrngo  21993  rngosn  21994  vcgrp  22039  vcoprnelem  22059  isvc  22062  isvci  22063  nvgrp  22098  cnnv  22170  cnnvba  22172  cncph  22322  hilid  22665  hhnv  22669  hhba  22671  hhph  22682  hhssabloi  22764  hhssnv  22766  ablo4pnp  26557  iscringd  26611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-cnv 4888  df-dm 4890  df-rn 4891  df-iota 5420  df-fv 5464  df-ov 6086  df-ablo 21872
  Copyright terms: Public domain W3C validator