Theorem grpmnd 17429

Description: A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
grpmnd	|- ( G e. Grp -> G e. Mnd )

Proof of Theorem grpmnd

Dummy variables m a are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- ( Base ` G ) = ( Base ` G )
2		eqid 2622	. . 3 |- ( +g ` G ) = ( +g ` G )
3		eqid 2622	. . 3 |- ( 0g ` G ) = ( 0g ` G )
4	1, 2, 3	isgrp 17428	. 2 |- ( G e. Grp <-> ( G e. Mnd /\ A. a e. ( Base ` G ) E. m e. ( Base ` G ) ( m ( +g ` G ) a ) = ( 0g ` G ) ) )
5	4	simplbi 476	1 |- ( G e. Grp -> G e. Mnd )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   0gc0g 16100   Mndcmnd 17294   Grpcgrp 17422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-grp 17425

This theorem is referenced by:  grpcl  17430  grpass  17431  grpideu  17433  grpplusf  17434  grpplusfo  17435  grpsgrp  17446  dfgrp2  17447  grpidcl  17450  grplid  17452  grprid  17453  dfgrp3  17514  prdsgrpd  17525  prdsinvgd  17526  ghmgrp  17539  mulgaddcom  17564  mulginvcom  17565  mulgz  17568  mulgdirlem  17572  mulgneg2  17575  mulgass  17579  issubg3  17612  subgacs  17629  ghmmhm  17670  0ghm  17674  pwsdiagghm  17688  cntzsubg  17769  oppggrp  17787  gsumccatsymgsn  17846  symggen  17890  symgtrinv  17892  psgnunilem5  17914  psgnunilem2  17915  psgnuni  17919  psgneldm2  17924  psgnfitr  17937  lsmass  18083  lsmcntzr  18093  pj1ghm  18116  frgpmhm  18178  frgpuplem  18185  frgpupf  18186  frgpup1  18188  isabl2  18201  isabld  18206  gsumzinv  18345  telgsumfzslem  18385  telgsumfzs  18386  dprdssv  18415  dprdfid  18416  dprdfadd  18419  dprdfeq0  18421  dprdlub  18425  dmdprdsplitlem  18436  dprddisj2  18438  dpjidcl  18457  pgpfac1lem3a  18475  pgpfaclem3  18482  ringmnd  18556  unitabl  18668  unitsubm  18670  lmodvsmmulgdi  18898  psgnghm  19926  dsmmsubg  20087  frlm0  20098  mdetunilem7  20424  istgp2  21895  symgtgp  21905  clmmulg  22901  dchrptlem3  24991  abliso  29696  isarchi3  29741  ofldchr  29814  reofld  29840  pwssplit4  37659  pwslnmlem2  37663  gicabl  37669  mendring  37762  c0ghm  41911  c0snghm  41916  lmodvsmdi  42163  lincvalsng  42205  lincvalsc0  42210  linc0scn0  42212  linc1  42214  lcoel0  42217  lincsum  42218  lincsumcl  42220  snlindsntor  42260