Theorem mndidcl 18686

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 18681	. 2 ⊢ (𝐺 ∈ Mnd → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐺)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐺)𝑥) = 𝑦))
5	1, 2, 3, 4	mgmidcl 18603	1 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Mndcmnd 18671

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 5243  ax-nul 5253  ax-pr 5379

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672

This theorem is referenced by:  mndbn0  18687  hashfinmndnn  18688  mndpfo  18694  mndpsuppss  18702  prdsidlem  18706  imasmnd  18712  xpsmnd0  18715  idmhm  18732  mhmf1o  18733  mndvlid  18736  mndvrid  18737  issubmd  18743  submid  18747  0subm  18754  0mhm  18756  mhmco  18760  mhmeql  18763  submacs  18764  mndind  18765  prdspjmhm  18766  pwsdiagmhm  18768  pwsco1mhm  18769  pwsco2mhm  18770  gsumvallem2  18771  dfgrp2  18904  grpidcl  18907  mhmid  19005  mhmmnd  19006  mulgnn0cl  19032  mulgnn0z  19043  cntzsubm  19279  oppgmnd  19295  gex1  19532  mulgnn0di  19766  mulgmhm  19768  subcmn  19778  gsumval3  19848  gsumzcl2  19851  gsumzaddlem  19862  gsumzsplit  19868  gsumzmhm  19878  gsummpt1n0  19906  simpgnideld  20042  submomnd  20073  omndmul2  20074  omndmul3  20075  omndmul  20076  ogrpinv0le  20077  gsumle  20086  srgidcl  20146  srg0cl  20147  ringidcl  20212  gsummgp0  20265  c0mgm  20407  c0mhm  20408  c0snmgmhm  20410  c0snmhm  20411  pwssplit1  21023  rngqiprngimf1  21267  dsmm0cl  21707  dsmmacl  21708  mhmcompl  22336  mdet0  22562  mndifsplit  22592  gsummatr01lem3  22613  pmatcollpw3fi1lem1  22742  tmdmulg  24048  tmdgsum  24051  tsms0  24098  tsmssplit  24108  tsmsxp  24111  mndlactfo  33120  mndractfo  33122  mndlactf1o  33123  mndractf1o  33124  suppgsumssiun  33166  gsumwun  33170  cntzsnid  33174  fxpsubm  33266  slmd0vcl  33315  ply1degltdimlem  33800  lvecendof1f1o  33811  sibf0  34512  sitmcl  34529  primrootsunit1  42467  primrootscoprmpow  42469  primrootscoprbij  42472  evl1gprodd  42487  ringexp0nn  42504  aks6d1c5lem2  42508  pwssplit4  43446  mgpsumz  48722  lco0  48787  mndtccatid  49946