Theorem grpmnd 13506

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 2209	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2209	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2209	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 13505	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺)))
5	4	simplbi 274	1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  ∀wral 2488  ∃wrex 2489  ‘cfv 5294  (class class class)co 5974  Basecbs 12998  +_gcplusg 13076  0_gc0g 13255  Mndcmnd 13415  Grpcgrp 13499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-rab 2497  df-v 2781  df-un 3181  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-iota 5254  df-fv 5302  df-ov 5977  df-grp 13502

This theorem is referenced by:  grpcl  13507  grpass  13508  grpideu  13510  grpmndd  13512  grpplusf  13514  grpplusfo  13515  grpsgrp  13524  dfgrp2  13526  grpidcl  13528  grplid  13530  grprid  13531  dfgrp3m  13598  prdsgrpd  13608  prdsinvgd  13609  mulgaddcom  13649  mulginvcom  13650  mulgz  13653  mulgneg2  13659  mulgass  13662  issubg3  13695  grpissubg  13697  0subg  13702  ghmex  13758  0ghm  13761  isabl2  13797