Theorem grpmnd 18862

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

Assertion

Ref	Expression
grpmnd	⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Proof of Theorem grpmnd

Dummy variables 𝑚 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2730	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2730	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2730	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 18861	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺)))
5	4	simplbi 496	1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ∀wral 3059  ∃wrex 3068  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  +_gcplusg 17201  0_gc0g 17389  Mndcmnd 18659  Grpcgrp 18855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-grp 18858

This theorem is referenced by:  grpcl  18863  grpass  18864  grpideu  18866  grpmndd  18868  grpplusf  18870  grpplusfo  18871  grpsgrp  18882  dfgrp2  18883  grpidcl  18886  grplid  18888  grprid  18889  dfgrp3  18958  prdsgrpd  18969  prdsinvgd  18970  mulgaddcom  19014  mulginvcom  19015  mulgz  19018  mulgneg2  19024  mulgass  19027  issubg3  19060  grpissubg  19062  0subg  19067  subgacs  19077  0ghm  19144  pwsdiagghm  19158  cntzsubg  19244  oppggrp  19265  symgsubmefmndALT  19312  psgnunilem5  19403  psgnuni  19408  0subgALT  19477  lsmcntzr  19589  pj1ghm  19612  isabl2  19699  cntrabl  19752  dprdfid  19928  dprdfeq0  19933  dprdlub  19937  dmdprdsplitlem  19948  dprddisj2  19950  dpjidcl  19969  pgpfaclem3  19994  simpgnideld  20010  c0ghm  20352  c0snghm  20355  dsmmsubg  21517  frlm0  21528  mdetunilem7  22340  istgp2  23815  cyc3genpm  32581  isarchi3  32603  ofldchr  32702  reofld  32729  lbslsat  32989  dimkerim  33000  fedgmullem2  33003  pwssplit4  42133  pwslnmlem2  42137  lcoel0  47196