Theorem cmnmnd 19890

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ‘cfv 6540  (class class class)co 7416  Basecbs 17286  +_gcplusg 17327  Mndcmnd 18813  CMndccmn 19873

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-cmn 19875

This theorem is used by:  cmn32  19893  cmn4  19894  cmn12  19895  cmnmndd  19897  rinvmod  19899  mulgnn0di  19918  mulgmhm  19920  ghmcmn  19924  prdscmnd  19954  gsumres  20006  gsumcl2  20007  gsumf1o  20009  gsumsubmcl  20012  gsumadd  20016  gsumsplit  20021  gsummhm  20031  gsummulglem  20034  gsuminv  20039  gsumpr  20048  gsumunsnfd  20050  gsumdifsnd  20054  gsum2d  20065  prdsgsum  20074  gsumle  20238  srgmnd  20295  gsumvsmul  21076  xrge0omnd  21624  frlmgsum  21951  frlmup2  21978  islindf4  22017  evlslem3  22260  mdetdiagid  22786  mdetrlin  22788  gsummatr01lem3  22843  gsummatr01  22845  chpscmat  23028  chp0mat  23032  chpidmat  23033  tmdgsum  24281  tmdgsum2  24282  tsms0  24328  tsmsmhm  24332  tsmsadd  24333  tgptsmscls  24336  tsmssplit  24338  tsmsxplem1  24339  tsmsxplem2  24340  imasdsf1olem  24559  lgseisenlem4  27571  xrge00  33357  gsumvsmul1  33394  gsummptres  33395  slmdmnd  33549  psrmonprod  33965  lbsdiflsp0  34039  xrge0iifmhm  34352  xrge0tmdALT  34359  esum0  34462  esumsnf  34477  esumcocn  34493  aks6d1c1  42916  aks6d1c5lem0  42935  aks6d1c5lem3  42937  aks6d1c5lem2  42938  aks6d1c5  42939  gsumge0cl  47118  sge0tsms  47127  gsumdifsndf  48979