Theorem mndidcl 18948

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6543  Basecbs 17396  +_gcplusg 17437  0_gc0g 17619  Mndcmnd 18932

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fv 6551  df-riota 7381  df-ov 7427  df-0g 17621  df-mgm 18825  df-sgrp 18917  df-mnd 18933

This theorem is used by:  mndbn0  18949  hashfinmndnn  18950  mndpfoOLD  18958  mndpsuppss  18968  prdsidlem  18972  imasmnd  18978  xpsmnd0  18981  idmhm  18999  mhmf1o  19000  mndvlid  19003  mndvrid  19004  issubmd  19010  submid  19014  0subm  19022  0mhm  19024  mhmco  19028  mhmeql  19031  submacs  19032  mndind  19033  prdspjmhm  19034  pwsdiagmhm  19036  pwsco1mhm  19037  pwsco2mhm  19038  gsumvallem2  19039  dfgrp2  19182  grpidcl  19185  mhmid  19282  mhmmnd  19283  mulgnn0cl  19309  mulgnn0z  19320  cntzsubm  19561  oppgmnd  19577  gex1  19814  mulgnn0di  20048  mulgmhm  20050  subcmn  20060  gsumval3  20130  gsumzcl2  20133  gsumzaddlem  20144  gsumzsplit  20150  gsumzmhm  20160  gsummpt1n0  20188  simpgnideld  20324  submomnd  20355  omndmul2  20356  omndmul3  20357  omndmul  20358  ogrpinv0le  20359  gsumle  20368  srgidcl  20434  srg0cl  20435  ringidcl  20503  gsummgp0  20556  c0mgm  20698  c0mhm  20699  c0snmgmhm  20701  c0snmhm  20702  pwssplit1  21343  rngqiprngimf1  21605  dsmm0cl  22055  dsmmacl  22056  mhmcompl  22439  mdet0  22930  mndifsplit  22960  gsummatr01lem3  22981  pmatcollpw3fi1lem1  23113  tmdmulg  24420  tmdgsum  24423  tsms0  24470  tsmssplit  24480  tsmsxp  24483  mndlactfo  33638  mndractfo  33640  mndlactf1o  33641  mndractf1o  33642  suppgsumssiun  33683  gsumwun  33687  cntzsnid  33691  fxpsubm  33783  slmd0vcl  33832  ply1degltdimlem  34304  lvecendof1f1o  34315  sibf0  35016  sitmcl  35033  primrootsunit1  43284  primrootscoprmpow  43286  primrootscoprbij  43289  evl1gprodd  43304  ringexp0nn  43321  aks6d1c5lem2  43325  pwssplit4  44228  mgpsumz  49610  lco0  49675  mndtccatid  50861