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

Theorem isabld 15151
Description: Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
Hypotheses
Ref Expression
isabld.b  |-  ( ph  ->  B  =  ( Base `  G ) )
isabld.p  |-  ( ph  ->  .+  =  ( +g  `  G ) )
isabld.g  |-  ( ph  ->  G  e.  Grp )
isabld.c  |-  ( (
ph  /\  x  e.  B  /\  y  e.  B
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
Assertion
Ref Expression
isabld  |-  ( ph  ->  G  e.  Abel )
Distinct variable groups:    x, y, B    x, G, y    ph, x, y
Allowed substitution hints:    .+ ( x, y)

Proof of Theorem isabld
StepHypRef Expression
1 isabld.g . 2  |-  ( ph  ->  G  e.  Grp )
2 isabld.b . . 3  |-  ( ph  ->  B  =  ( Base `  G ) )
3 isabld.p . . 3  |-  ( ph  ->  .+  =  ( +g  `  G ) )
4 grpmnd 14543 . . . 4  |-  ( G  e.  Grp  ->  G  e.  Mnd )
51, 4syl 15 . . 3  |-  ( ph  ->  G  e.  Mnd )
6 isabld.c . . 3  |-  ( (
ph  /\  x  e.  B  /\  y  e.  B
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
72, 3, 5, 6iscmnd 15150 . 2  |-  ( ph  ->  G  e. CMnd )
8 isabl 15142 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
91, 7, 8sylanbrc 645 1  |-  ( ph  ->  G  e.  Abel )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    = wceq 1633    e. wcel 1701   ` cfv 5292  (class class class)co 5900   Basecbs 13195   +g cplusg 13255   Mndcmnd 14410   Grpcgrp 14411  CMndccmn 15138   Abelcabel 15139
This theorem is referenced by:  subgabl  15181  gex2abl  15192  cygabl  15226  rngabl  15419  lmodabl  15721  dchrabl  20546  tgrpabl  30758  erngdvlem2N  30996  erngdvlem2-rN  31004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-grp 14538  df-cmn 15140  df-abl 15141
  Copyright terms: Public domain W3C validator