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

Theorem ablogrpo 20951
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 2283 . . 3  |-  ran  G  =  ran  G
21isablo 20950 . 2  |-  ( G  e.  AbelOp 
<->  ( G  e.  GrpOp  /\ 
A. x  e.  ran  G A. y  e.  ran  G ( x G y )  =  ( y G x ) ) )
32simplbi 446 1  |-  ( G  e.  AbelOp  ->  G  e.  GrpOp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   A.wral 2543   ran crn 4690  (class class class)co 5858   GrpOpcgr 20853   AbelOpcablo 20948
This theorem is referenced by:  ablo32  20953  ablo4  20954  ablomuldiv  20956  ablodivdiv  20957  ablodivdiv4  20958  ablonnncan  20960  ablonncan  20961  ablonnncan1  20962  gxdi  20963  cnid  21018  addinv  21019  readdsubgo  21020  zaddsubgo  21021  mulid  21023  ghablo  21036  efghgrp  21040  rngogrpo  21057  cnrngo  21070  rngosn  21071  vcgrp  21114  vcoprnelem  21134  isvc  21137  isvci  21138  nvgrp  21173  cnnv  21245  cnnvba  21247  cncph  21397  hilid  21740  hhnv  21744  hhba  21746  hhph  21757  hhssabloi  21839  hhssnv  21841  abloinvop  25353  fprodneg  25378  fprodsub  25379  clfsebs5  25382  rngoinvcl  25421  zintdom  25438  claddinvvec  25460  vec2inv  25461  sum2vv  25462  addnull1  25463  addnull2  25464  addvecass  25465  invaddvec  25467  vecsrcan  25469  vecslcan  25470  vwit  25471  sub2vec  25472  mvecrtol  25473  vecrcan  25475  veclcan  25476  mvecrtol2  25477  mulinvsca  25480  muldisc  25481  svli2  25484  svs2  25487  ablo4pnp  26570  iscringd  26624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700  df-iota 5219  df-fv 5263  df-ov 5861  df-ablo 20949
  Copyright terms: Public domain W3C validator