grpidcl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > grpidcl		Structured version Visualization version GIF version

Theorem grpidcl 18948

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 = (0_g‘𝐺)

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

**Proof of Theorem grpidcl**
Step	Hyp	Ref	Expression
1		grpmnd 18923	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpidcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpidcl.o	. . 3 ⊢ 0 = (0_g‘𝐺)
4	2, 3	mndidcl 18727	. 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 17	1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ‘cfv 6531 Basecbs 17228 0_gc0g 17453 Mndcmnd 18712 Grpcgrp 18916

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-dif 3929 df-un 3931 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-iota 6484 df-fun 6533 df-fv 6539 df-riota 7362 df-ov 7408 df-0g 17455 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-grp 18919

This theorem is referenced by: grpbn0 18949 grprcan 18956 grpid 18958 isgrpid2 18959 grprinv 18973 grpidinv 18981 grpinvid 18982 grpidrcan 18986 grpidlcan 18987 grpidssd 18999 grpinvval2 19006 grpsubid1 19008 imasgrp 19039 mulgcl 19074 mulgz 19085 subg0 19115 subg0cl 19117 issubg4 19128 0subgOLD 19135 nmzsubg 19148 eqgid 19163 eqg0el 19166 qusgrp 19169 qus0 19172 ghmid 19205 ghmpreima 19221 f1ghm0to0 19228 kerf1ghm 19230 ghmqusker 19270 gafo 19279 gaid 19282 gass 19284 gaorber 19291 gastacl 19292 lactghmga 19386 cayleylem2 19394 symgsssg 19448 symgfisg 19449 od1 19540 gexdvds 19565 sylow1lem2 19580 sylow3lem1 19608 lsmdisj2 19663 0frgp 19760 odadd1 19829 torsubg 19835 oddvdssubg 19836 0cyg 19874 prmcyg 19875 telgsums 19974 dprdfadd 20003 dprdz 20013 pgpfac1lem3a 20059 ablsimpgprmd 20098 rng0cl 20123 rnglz 20125 rngrz 20126 ring0cl 20227 zrrnghm 20496 isdomn4 20676 isdrng2 20703 srng0 20814 lmod0vcl 20848 islmhm2 20996 rnglidl0 21190 frgpcyg 21534 ip0l 21596 ocvlss 21632 ascl0 21844 psr0cl 21912 mplsubglem 21959 mhp0cl 22084 mhpaddcl 22089 evl1gsumd 22295 grpvlinv 22336 matinvgcell 22373 mat0dim0 22405 mdetdiag 22537 mdetuni0 22559 chpdmatlem2 22777 chp0mat 22784 istgp2 24029 cldsubg 24049 tgpconncompeqg 24050 tgpconncomp 24051 snclseqg 24054 tgphaus 24055 tgpt1 24056 qustgphaus 24061 tgptsmscls 24088 nrmmetd 24513 nmfval2 24530 nmval2 24531 nmf2 24532 ngpds3 24547 nmge0 24556 nmeq0 24557 nminv 24560 nmmtri 24561 nmrtri 24563 nm0 24568 tngnm 24590 idnghm 24682 nmcn 24784 clmvz 25062 nmoleub2lem2 25067 nglmle 25254 mdeg0 26027 dchrinv 27224 dchr1re 27226 dchrpt 27230 dchrsum2 27231 dchrhash 27234 rpvmasumlem 27450 rpvmasum2 27475 dchrisum0re 27476 ogrpinv0lt 33090 ogrpinvlt 33091 isarchi3 33185 archirng 33186 archirngz 33187 archiabllem1b 33190 rmfsupp2 33233 erler 33260 rlocaddval 33263 rlocmulval 33264 rloc0g 33266 fracfld 33302 orngsqr 33326 ornglmulle 33327 orngrmulle 33328 ornglmullt 33329 orngrmullt 33330 orngmullt 33331 ofldchr 33336 isarchiofld 33339 qusker 33364 grplsm0l 33418 qus0g 33422 nsgqus0 33425 nsgmgclem 33426 fedgmullem1 33669 irredminply 33750 rtelextdg2lem 33760 qqh0 34015 sconnpi1 35261 lfl0f 39087 lkrlss 39113 lshpkrlem1 39128 lkrin 39182 dvhgrp 41126 primrootscoprmpow 42112 aks5lem7 42213 fsuppind 42613 fsuppssind 42616 mhpind 42617 evl1at0 48367

W3C validator