MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mndidcl Structured version   Unicode version

Theorem mndidcl 15550
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  |-  B  =  ( Base `  G
)
mndidcl.o  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
mndidcl  |-  ( G  e.  Mnd  ->  .0.  e.  B )

Proof of Theorem mndidcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mndidcl.b . 2  |-  B  =  ( Base `  G
)
2 mndidcl.o . 2  |-  .0.  =  ( 0g `  G )
3 eqid 2451 . 2  |-  ( +g  `  G )  =  ( +g  `  G )
41, 3mndid 15533 . 2  |-  ( G  e.  Mnd  ->  E. x  e.  B  A. y  e.  B  ( (
x ( +g  `  G
) y )  =  y  /\  ( y ( +g  `  G
) x )  =  y ) )
51, 2, 3, 4mgmidcl 15547 1  |-  ( G  e.  Mnd  ->  .0.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   ` cfv 5519   Basecbs 14285   +g cplusg 14349   0gc0g 14489   Mndcmnd 15520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-iota 5482  df-fun 5521  df-fv 5527  df-riota 6154  df-ov 6196  df-0g 14491  df-mnd 15526
This theorem is referenced by:  mndfo  15556  prdsidlem  15564  imasmnd  15570  mhmf1o  15584  issubmd  15588  submid  15590  0mhm  15597  mhmco  15601  mhmeql  15603  submacs  15604  mrcmndind  15605  prdspjmhm  15606  pwsdiagmhm  15608  pwsco1mhm  15609  pwsco2mhm  15610  gsumvallem2  15612  grpidcl  15677  mulgnn0cl  15754  mulgnn0z  15758  cntzsubm  15964  oppgmnd  15980  gex1  16203  mulgnn0di  16426  mulgmhm  16428  subcmn  16434  gsumval3OLD  16495  gsumval3  16498  gsumzcl2  16502  gsumzclOLD  16506  gsumzaddlem  16521  gsumzaddlemOLD  16523  gsumzsplit  16531  gsumzsplitOLD  16532  gsumzmhm  16544  gsumzmhmOLD  16545  gsummpt1n0  16570  srgidcl  16733  srg0cl  16734  rngidcl  16780  gsummgp0  16814  pwssplit1  17255  dsmm0cl  18283  dsmmacl  18284  mndvlid  18411  mndvrid  18412  mdet0  18537  mndifsplit  18567  gsummatr01lem3  18588  tmdmulg  19788  tmdgsum  19791  tsms0  19840  tsmssplit  19851  tsmsxp  19854  submomnd  26311  omndmul2  26313  omndmul3  26314  omndmul  26315  ogrpinv0le  26317  slmdbn0  26362  slmdsn0  26365  slmd0vcl  26375  gsumle  26384  sibf0  26857  pwssplit4  29583  mgpsumz  30901  mndpsuppss  30925  lco0  31071  pmatcollpw4fi1lem1  31245
  Copyright terms: Public domain W3C validator