Theorem grpidcl 13583

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

Hypotheses

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

Assertion

Ref	Expression
grpidcl	⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Proof of Theorem grpidcl

Step	Hyp	Ref	Expression
1		grpmnd 13561	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpidcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpidcl.o	. . 3 ⊢ 0 = (0g‘𝐺)
4	2, 3	mndidcl 13484	. 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 14	1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  ‘cfv 5321  Basecbs 13053  0_gc0g 13310  Mndcmnd 13470  Grpcgrp 13554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294  ax-un 4525  ax-cnex 8106  ax-resscn 8107  ax-1re 8109  ax-addrcl 8112

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-rn 4731  df-res 4732  df-iota 5281  df-fun 5323  df-fn 5324  df-fv 5329  df-riota 5963  df-ov 6013  df-inn 9127  df-2 9185  df-ndx 13056  df-slot 13057  df-base 13059  df-plusg 13144  df-0g 13312  df-mgm 13410  df-sgrp 13456  df-mnd 13471  df-grp 13557

This theorem is referenced by:  grpbn0  13584  grprcan  13591  grpid  13593  isgrpid2  13594  grprinv  13605  grpidinv  13613  grpinvid  13614  grpressid  13615  grpidrcan  13619  grpidlcan  13620  grpidssd  13630  grpinvval2  13637  grpsubid1  13639  dfgrp3m  13653  grpsubpropd2  13659  imasgrp  13669  mulgcl  13697  mulgz  13708  subg0  13738  subg0cl  13740  issubg2m  13747  issubg4m  13751  grpissubg  13752  subgintm  13756  0subg  13757  nmzsubg  13768  0nsg  13772  triv1nsgd  13776  eqgid  13784  eqg0el  13787  qusgrp  13790  qus0  13793  ghmid  13807  ghmrn  13815  ghmpreima  13824  f1ghm0to0  13830  kerf1ghm  13832  rng0cl  13927  rnglz  13929  rngrz  13930  ring0cl  14005  ringlz  14027  ringrz  14028  lmod0vcl  14302  lmodfopnelem1  14309  rmodislmodlem  14335  rmodislmod  14336  islss3  14364  psr0cl  14666  psr0lid  14667  mplsubgfilemm  14683