Theorem mndidcl 18711

Description: The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)

Hypotheses

Ref	Expression
mndidcl.b	⊢ 𝐵 = (Base‘𝐺)
mndidcl.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
mndidcl	⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Proof of Theorem mndidcl

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

Step	Hyp	Ref	Expression
1		mndidcl.b	. 2 ⊢ 𝐵 = (Base‘𝐺)
2		mndidcl.o	. 2 ⊢ 0 = (0g‘𝐺)
3		eqid 2737	. 2 ⊢ (+g‘𝐺) = (+g‘𝐺)
4	1, 3	mndid 18706	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 18628	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  Basecbs 17173  +_gcplusg 17214  0_gc0g 17396  Mndcmnd 18696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-riota 7318  df-ov 7364  df-0g 17398  df-mgm 18602  df-sgrp 18681  df-mnd 18697

This theorem is referenced by:  mndbn0  18712  hashfinmndnn  18713  mndpfo  18719  mndpsuppss  18727  prdsidlem  18731  imasmnd  18737  xpsmnd0  18740  idmhm  18757  mhmf1o  18758  mndvlid  18761  mndvrid  18762  issubmd  18768  submid  18772  0subm  18779  0mhm  18781  mhmco  18785  mhmeql  18788  submacs  18789  mndind  18790  prdspjmhm  18791  pwsdiagmhm  18793  pwsco1mhm  18794  pwsco2mhm  18795  gsumvallem2  18796  dfgrp2  18932  grpidcl  18935  mhmid  19033  mhmmnd  19034  mulgnn0cl  19060  mulgnn0z  19071  cntzsubm  19307  oppgmnd  19323  gex1  19560  mulgnn0di  19794  mulgmhm  19796  subcmn  19806  gsumval3  19876  gsumzcl2  19879  gsumzaddlem  19890  gsumzsplit  19896  gsumzmhm  19906  gsummpt1n0  19934  simpgnideld  20070  submomnd  20101  omndmul2  20102  omndmul3  20103  omndmul  20104  ogrpinv0le  20105  gsumle  20114  srgidcl  20174  srg0cl  20175  ringidcl  20240  gsummgp0  20291  c0mgm  20433  c0mhm  20434  c0snmgmhm  20436  c0snmhm  20437  pwssplit1  21049  rngqiprngimf1  21293  dsmm0cl  21733  dsmmacl  21734  mhmcompl  22358  mdet0  22584  mndifsplit  22614  gsummatr01lem3  22635  pmatcollpw3fi1lem1  22764  tmdmulg  24070  tmdgsum  24073  tsms0  24120  tsmssplit  24130  tsmsxp  24133  mndlactfo  33105  mndractfo  33107  mndlactf1o  33108  mndractf1o  33109  suppgsumssiun  33151  gsumwun  33155  cntzsnid  33159  fxpsubm  33251  slmd0vcl  33300  ply1degltdimlem  33785  lvecendof1f1o  33796  sibf0  34497  sitmcl  34514  primrootsunit1  42553  primrootscoprmpow  42555  primrootscoprbij  42558  evl1gprodd  42573  ringexp0nn  42590  aks6d1c5lem2  42594  pwssplit4  43538  mgpsumz  48853  lco0  48918  mndtccatid  50077