Theorem cmnmnd 19402

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

Assertion

Ref	Expression
cmnmnd	⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Proof of Theorem cmnmnd

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2738	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	iscmn 19394	. 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))
4	3	simplbi 498	1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  +_gcplusg 16962  Mndcmnd 18385  CMndccmn 19386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-cmn 19388

This theorem is referenced by:  cmn32  19405  cmn4  19406  cmn12  19407  cmnmndd  19409  rinvmod  19410  mulgnn0di  19427  mulgmhm  19429  ghmcmn  19433  prdscmnd  19462  gsumres  19514  gsumcl2  19515  gsumf1o  19517  gsumsubmcl  19520  gsumadd  19524  gsumsplit  19529  gsummhm  19539  gsummulglem  19542  gsuminv  19547  gsumpr  19556  gsumunsnfd  19558  gsumdifsnd  19562  gsum2d  19573  prdsgsum  19582  srgmnd  19745  gsumvsmul  20187  frlmgsum  20979  frlmup2  21006  islindf4  21045  evlslem3  21290  mdetdiagid  21749  mdetrlin  21751  mdetrsca  21752  gsummatr01lem3  21806  gsummatr01  21808  chpscmat  21991  chp0mat  21995  chpidmat  21996  tmdgsum  23246  tmdgsum2  23247  tsms0  23293  tsmsmhm  23297  tsmsadd  23298  tgptsmscls  23301  tsmssplit  23303  tsmsxplem1  23304  tsmsxplem2  23305  imasdsf1olem  23526  lgseisenlem4  26526  xrge00  31295  gsumvsmul1  31311  gsummptres  31312  xrge0omnd  31337  gsumle  31350  slmdmnd  31459  lbsdiflsp0  31707  xrge0iifmhm  31889  xrge0tmdALT  31896  esum0  32017  esumsnf  32032  esumcocn  32048  gsumge0cl  43909  sge0tsms  43918  gsumdifsndf  45375