Theorem cmnmnd 19778

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 2735	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2735	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	iscmn 19770	. 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))
4	3	simplbi 497	1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  +_gcplusg 17271  Mndcmnd 18712  CMndccmn 19761

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-cmn 19763

This theorem is referenced by:  cmn32  19781  cmn4  19782  cmn12  19783  cmnmndd  19785  rinvmod  19787  mulgnn0di  19806  mulgmhm  19808  ghmcmn  19812  prdscmnd  19842  gsumres  19894  gsumcl2  19895  gsumf1o  19897  gsumsubmcl  19900  gsumadd  19904  gsumsplit  19909  gsummhm  19919  gsummulglem  19922  gsuminv  19927  gsumpr  19936  gsumunsnfd  19938  gsumdifsnd  19942  gsum2d  19953  prdsgsum  19962  srgmnd  20150  gsumvsmul  20883  frlmgsum  21732  frlmup2  21759  islindf4  21798  evlslem3  22038  mdetdiagid  22538  mdetrlin  22540  gsummatr01lem3  22595  gsummatr01  22597  chpscmat  22780  chp0mat  22784  chpidmat  22785  tmdgsum  24033  tmdgsum2  24034  tsms0  24080  tsmsmhm  24084  tsmsadd  24085  tgptsmscls  24088  tsmssplit  24090  tsmsxplem1  24091  tsmsxplem2  24092  imasdsf1olem  24312  lgseisenlem4  27341  xrge00  33007  gsumvsmul1  33045  gsummptres  33046  xrge0omnd  33079  gsumle  33092  slmdmnd  33203  lbsdiflsp0  33666  xrge0iifmhm  33970  xrge0tmdALT  33977  esum0  34080  esumsnf  34095  esumcocn  34111  aks6d1c1  42129  aks6d1c5lem0  42148  aks6d1c5lem3  42150  aks6d1c5lem2  42151  aks6d1c5  42152  gsumge0cl  46400  sge0tsms  46409  gsumdifsndf  48156